theorem Th36: :: EUCLID_8:44

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>)