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;
reconsider f1 = (f . 1) ^2 , f2 = (f . 2) ^2 as Element of REAL by XREAL_0:def 1;
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:44;
then Sum (sqr f) = Sum (<*f1*> ^ <*f2*>) by FINSEQ_1:def 9
.= (Sum <*f1*>) + ((f . 2) ^2) by RVSUM_1:74
.= ((f . 1) ^2) + ((f . 2) ^2) by RVSUM_1:73 ;
hence |.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2)) ; :: thesis: verum