theorem :: BKMODEL1:24

for m, n being Nat
for M being Matrix of m,F_Real
for N being Matrix of m,n,F_Real st m > 0 holds
M * N is Matrix of m,n,F_Real