let M be Matrix of INT; :: thesis: M is Matrix of REAL
INT * c= REAL * by NUMBERS:15, FINSEQ_1:62;
then rng M c= REAL * ;
hence M is Matrix of REAL by FINSEQ_1:def 4; :: thesis: verum