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