:: deftheorem Def3 defines Mx2Tran MATRTOP1:def 3 :
for n, m being Nat
for M being Matrix of n,m,F_Real
for b₄ being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 implies ( b₄ = Mx2Tran M iff for f being b₁ -element real-valued FinSequence holds b₄ . f = Line (((LineVec2Mx (@ f)) * M),1) ) ) & ( not n <> 0 implies ( b₄ = Mx2Tran M iff for f being b₁ -element real-valued FinSequence holds b₄ . f = 0. (TOP-REAL m) ) ) );