theorem Th33: :: MATRLIN2:33

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 v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2