theorem :: ANPROJ_8:94

for p, q, r being Point of (TOP-REAL 3)
for pf, qf, rf being FinSequence of F_Real st p = pf & q = qf & r = rf & |{p,q,r}| <> 0 holds
ex M being Matrix of 3,F_Real st
( M is invertible & M * pf = F2M <e1> & M * qf = F2M <e2> & M * rf = F2M <e3> )