theorem :: EUCLID_8:45

for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>)