let n be Nat; :: thesis: for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
let p, q be Element of n -tuples_on REAL; :: thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
|((p - q),(p - q))| = ((|(p,p)| - |(p,q)|) - |(p,q)|) + |(q,q)| by Th137
.= (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ;
hence |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; :: thesis: verum