for n, m being Nat
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)