theorem Th78: :: ANPROJ_8:97

for p, q, r being Point of (TOP-REAL 3)
for M being Matrix of 3,F_Real
for pm, qm, rm being Point of (TOP-REAL 3)
for pt, qt, rt being FinSequence of 1 -tuples_on REAL
for pf, qf, rf being FinSequence of F_Real st M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm holds
( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )