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:2;
then A1:
((p + q) `1) ^2 = (((p `1) ^2) + ((2 * (p `1)) * (q `1))) + ((q `1) ^2)
by SQUARE_1:4;
(p + q) `2 = (p `2) + (q `2)
by TOPREAL3:2;
then A2:
((p + q) `2) ^2 = (((p `2) ^2) + ((2 * (p `2)) * (q `2))) + ((q `2) ^2)
by SQUARE_1:4;
(p - q) `2 = (p `2) - (q `2)
by TOPREAL3:3;
then A3:
((p - q) `2) ^2 = (((p `2) ^2) - ((2 * (p `2)) * (q `2))) + ((q `2) ^2)
by SQUARE_1:5;
(p - q) `1 = (p `1) - (q `1)
by TOPREAL3:3;
then A4:
((p - q) `1) ^2 = (((p `1) ^2) - ((2 * (p `1)) * (q `1))) + ((q `1) ^2)
by SQUARE_1:5;
|(p,q)| =
(1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
by EUCLID_2:49
.=
(1 / 4) * (((((p + q) `1) ^2) + (((p + q) `2) ^2)) - (|.(p - q).| ^2))
by JGRAPH_3:1
.=
(1 / 4) * (((((p + q) `1) ^2) + (((p + q) `2) ^2)) - ((((p - q) `1) ^2) + (((p - q) `2) ^2)))
by JGRAPH_3:1
.=
(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