for M being Matrix of 3,F_Real
for MR being Matrix of 3,REAL
for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for ufr being FinSequence of REAL
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds
v = MR * ufr