let n be Nat; :: thesis: for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
let x, y be Element of REAL n; :: thesis: |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
thus |((x - y),(x - y))| = ((|(x,x)| - |(x,y)|) - |(y,x)|) + |(y,y)| by Th31
.= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ; :: thesis: verum