set T = Mx2Tran M;
( @ f is FinSequence of REAL & len f = n ) by CARD_1:def 7;
then f is Element of n -tuples_on REAL by FINSEQ_2:92;
then f in REAL n ;
then f in the carrier of (TOP-REAL n) by EUCLID:22;
then f in dom (Mx2Tran M) by FUNCT_2:def 1;
then A1: (Mx2Tran M) . f in rng (Mx2Tran M) by FUNCT_1:def 3;
rng (Mx2Tran M) c= the carrier of (TOP-REAL m) by RELAT_1:def 19;
hence (Mx2Tran M) . f is m -element by A1; :: thesis: verum