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:22;
A1: (sqr w) . 2 = (p `2) ^2 by VALUED_1:11;
0 <= Sum (sqr w) by RVSUM_1:86;
then A2: |.p.| ^2 = Sum (sqr w) by SQUARE_1:def 2;
( len (sqr w) = 2 & (sqr w) . 1 = (p `1) ^2 ) by CARD_1:def 7, VALUED_1:11;
then sqr w = <*((p `1) ^2),((p `2) ^2)*> by A1, FINSEQ_1:44;
hence |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2) by A2, RVSUM_1:77; :: thesis: verum