let f be real-valued FinSequence; :: thesis: |.(- f).| = |.f.|
thus |.(- f).| = sqrt (Sum (sqr (abs (- f)))) by Lm2
.= sqrt (Sum (sqr (abs f))) by Th2
.= |.f.| by Lm2 ; :: thesis: verum