theorem Th32: :: EUCLID_4:32

for n being Nat
for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|