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 Th30
.= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| ; :: thesis: verum