theorem Th6: :: EUCLID_5:6

for x1, x2, y1, y2, z1, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|