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:44;
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:74
.= ((f . 1) ^2) + ((f . 2) ^2) by RVSUM_1:73 ;
hence |.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2)) ; :: thesis: verum