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

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