:: deftheorem defines inttorealM ZMATRLIN:def 1 :
for M being Matrix of INT holds inttorealM M = M;