theorem :: EUCLID_4:28

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