theorem Th24: :: MATRTOP1:24

for n, m being Nat
for f1, f2 being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)