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