theorem Th18: :: MATRTOP1:18

for n, m, i being Nat
for f being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))