let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2))
let p, q be Point of (TOP-REAL n); :: thesis: (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2))
A1: ((|.p.| ^2) - (2 * |(p,q)|)) + (|.q.| ^2) = ((|.p.| ^2) + (|.q.| ^2)) - (2 * |(p,q)|) ;
(|.(p + q).| ^2) + (|.(p - q).| ^2) = (((|.p.| ^2) + (2 * |(p,q)|)) + (|.q.| ^2)) + (|.(p - q).| ^2) by Th67
.= (((|.p.| ^2) + (|.q.| ^2)) + (2 * |(p,q)|)) + (((|.p.| ^2) + (|.q.| ^2)) - (2 * |(p,q)|)) by A1, Th68
.= 2 * ((|.p.| ^2) + (|.q.| ^2)) ;
hence (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * ((|.p.| ^2) + (|.q.| ^2)) ; :: thesis: verum