theorem :: EUCLID_8:41

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