:: deftheorem Def3 defines Mx2Tran MATRLIN2:def 3 :
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for b₇ being Function of V1,V2 holds
( b₇ = Mx2Tran (M,b1,B2) iff for v being Vector of V1 holds b₇ . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) );