let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n) holds |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2))
let p1, p2 be Point of (TOP-REAL n); :: thesis: |(p1,p2)| = (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2))
reconsider q1 = p1, q2 = p2 as Element of REAL n by EUCLID:22;
A1: p1 - p2 = q1 - q2 by EUCLID:69;
thus |(p1,p2)| = (1 / 4) * ((|.(q1 + q2).| ^2) - (|.(q1 - q2).| ^2)) by Th10
.= (1 / 4) * ((|.(p1 + p2).| ^2) - (|.(p1 - p2).| ^2)) by A1, EUCLID:64 ; :: thesis: verum