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 Th67
.= (((|.p.| ^2 ) + (2 * |(p,q)|)) + (|.q.| ^2 )) - (((|.p.| ^2 ) - (2 * |(p,q)|)) + (|.q.| ^2 )) by Th68
.= 4 * |(p,q)| ;
hence |(p,q)| = (1 / 4) * ((|.(p + q).| ^2 ) - (|.(p - q).| ^2 )) ; :: thesis: verum