theorem Th30: :: EUCLID_4:30

for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|