let p, q be Point of (TOP-REAL 2); |(p,q)| = ((p `1 ) * (q `1 )) + ((p `2 ) * (q `2 ))
(p + q) `1 = (p `1 ) + (q `1 )
by TOPREAL3:7;
then A1:
((p + q) `1 ) ^2 = (((p `1 ) ^2 ) + ((2 * (p `1 )) * (q `1 ))) + ((q `1 ) ^2 )
by SQUARE_1:63;
(p + q) `2 = (p `2 ) + (q `2 )
by TOPREAL3:7;
then A2:
((p + q) `2 ) ^2 = (((p `2 ) ^2 ) + ((2 * (p `2 )) * (q `2 ))) + ((q `2 ) ^2 )
by SQUARE_1:63;
(p - q) `2 = (p `2 ) - (q `2 )
by TOPREAL3:8;
then A3:
((p - q) `2 ) ^2 = (((p `2 ) ^2 ) - ((2 * (p `2 )) * (q `2 ))) + ((q `2 ) ^2 )
by SQUARE_1:64;
(p - q) `1 = (p `1 ) - (q `1 )
by TOPREAL3:8;
then A4:
((p - q) `1 ) ^2 = (((p `1 ) ^2 ) - ((2 * (p `1 )) * (q `1 ))) + ((q `1 ) ^2 )
by SQUARE_1:64;
|(p,q)| =
(1 / 4) * ((|.(p + q).| ^2 ) - (|.(p - q).| ^2 ))
by EUCLID_2:71
.=
(1 / 4) * (((((p + q) `1 ) ^2 ) + (((p + q) `2 ) ^2 )) - (|.(p - q).| ^2 ))
by JGRAPH_3:10
.=
(1 / 4) * (((((p + q) `1 ) ^2 ) + (((p + q) `2 ) ^2 )) - ((((p - q) `1 ) ^2 ) + (((p - q) `2 ) ^2 )))
by JGRAPH_3:10
.=
(1 / 4) * (((((p + q) `1 ) ^2 ) - (((p - q) `1 ) ^2 )) + ((((p + q) `2 ) ^2 ) - (((p - q) `2 ) ^2 )))
;
hence
|(p,q)| = ((p `1 ) * (q `1 )) + ((p `2 ) * (q `2 ))
by A1, A2, A4, A3; verum