let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2 ) - (|.(p - q).| ^2 ) = 4 * |(p,q)|
let p, q be Point of (TOP-REAL n); :: thesis: (|.(p + q).| ^2 ) - (|.(p - q).| ^2 ) = 4 * |(p,q)|
(|.(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).| ^2 ) - (|.(p - q).| ^2 ) = 4 * |(p,q)| ; :: thesis: verum