:: deftheorem defines inttorealM ZMODLAT1:def 33 :
for M being Matrix of INT.Ring holds inttorealM M = M;