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