theorem :: EUCLID_8:43

for p1, p2 being Element of REAL 3 holds p1 + p2 = ((((p1 . 1) + (p2 . 1)) * <e1>) + (((p1 . 2) + (p2 . 2)) * <e2>)) + (((p1 . 3) + (p2 . 3)) * <e3>)