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