for n, m, k being Nat
for A being Matrix of n,m,F_Real
for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)