let p be Point of (TOP-REAL 2); :: thesis: |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 )
reconsider w = p as Element of REAL 2 by EUCLID:25;
0 <= Sum (sqr w) by RVSUM_1:116;
then A1: |.p.| ^2 = Sum (sqr w) by SQUARE_1:def 4;
A2: len (sqr w) = 2 by FINSEQ_1:def 18;
A3: (sqr w) . 1 = (p `1 ) ^2 by VALUED_1:11;
(sqr w) . 2 = (p `2 ) ^2 by VALUED_1:11;
then sqr w = <*((p `1 ) ^2 ),((p `2 ) ^2 )*> by A2, A3, FINSEQ_1:61;
hence |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by A1, RVSUM_1:107; :: thesis: verum