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