theorem :: EUCLID_8:37

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