theorem Th77: :: ANPROJ_8:95

for p, q, r being Point of (TOP-REAL 3)
for M, PQR being Matrix of 3,F_Real
for pf, qf, rf being FinSequence of F_Real
for pt, qt, rt being FinSequence of 1 -tuples_on REAL st PQR = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf holds
(M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*>