theorem :: EUCLID_8:47

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