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 Th53
.= ((|.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