theorem MLT1: :: ZMODLAT1:94

for m, l, n being Nat
for S being Matrix of l,m,INT.Ring
for T being Matrix of m,n,INT.Ring
for S1 being Matrix of l,m,F_Real
for T1 being Matrix of m,n,F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds
S * T = S1 * T1