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