theorem Th22: :: MATRTOP1:22

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)