You are right, the lines in the proof are very long because the definitions (class variables in $e-Statements) of the lemmata used in the proof are expanded (I only kept the definitions which are required to formulate the theorem, not considering the proof...).
Maybe I should provide a second version of the theorem having more definitions, and therefore shorter lines in the proof, so that the proof becomes clearer. Alexander On Tuesday, November 26, 2019 at 6:05:17 PM UTC+1, Jon P wrote: > > Nice work :) > > The lines in the proof are amazingly long. I also think this from the end > of line 72 shows some epic nesting "𝑙))))))))‘𝑛))))) = 0 )" > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2f3c11c1-6854-4b9f-8f39-01b0faec7172%40googlegroups.com.
