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