for n, m, k being Nat
for f being b₁ -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being b₃ -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)