let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
let p, q be Point of (TOP-REAL n); :: thesis: |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
(|.(p + q).| ^2) - (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (|.(p - q).| ^2) by Th43
.= (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) - (((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2)) by Th44
.= 4 * |(p,q)| ;
hence |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2)) ; :: thesis: verum