let f be FinSequence of REAL ; :: thesis: ( len f = 2 implies |.f.| = sqrt (((f . 1) ^2 ) + ((f . 2) ^2 )) )
A1: ( (sqr f) . 1 = (f . 1) ^2 & (sqr f) . 2 = (f . 2) ^2 ) by VALUED_1:11;
( dom (sqr f) = dom f & Seg (len (sqr f)) = dom (sqr f) ) by FINSEQ_1:def 3, VALUED_1:11;
then A2: len (sqr f) = len f by FINSEQ_1:def 3;
assume len f = 2 ; :: thesis: |.f.| = sqrt (((f . 1) ^2 ) + ((f . 2) ^2 ))
then sqr f = <*((f . 1) ^2 ),((f . 2) ^2 )*> by A1, A2, 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