let f be FinSequence of REAL ; :: thesis: ( len f = 2 implies |.f.| = sqrt (((f . 1) ^2 ) + ((f . 2) ^2 )) )
assume A1: len f = 2 ; :: thesis: |.f.| = sqrt (((f . 1) ^2 ) + ((f . 2) ^2 ))
A2: (sqr f) . 1 = (f . 1) ^2 by VALUED_1:11;
A3: (sqr f) . 2 = (f . 2) ^2 by VALUED_1:11;
A4: dom (sqr f) = dom f by VALUED_1:11;
Seg (len (sqr f)) = dom (sqr f) by FINSEQ_1:def 3;
then len (sqr f) = len f by A4, FINSEQ_1:def 3;
then sqr f = <*((f . 1) ^2 ),((f . 2) ^2 )*> by A1, A2, A3, FINSEQ_1:61;
then Sum (sqr f) = Sum (<*((f . 1) ^2 )*> ^ <*((f . 2) ^2 )*>) by FINSEQ_1:def 9
.= (Sum <*((f . 1) ^2 )*>) + ((f . 2) ^2 ) by RVSUM_1:104
.= ((f . 1) ^2 ) + ((f . 2) ^2 ) by RVSUM_1:103 ;
hence |.f.| = sqrt (((f . 1) ^2 ) + ((f . 2) ^2 )) ; :: thesis: verum