let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real holds
( Mx2Tran M is onto iff the_rank_of M = m )
let M be Matrix of n,m,F_Real; :: thesis: ( Mx2Tran M is onto iff the_rank_of M = m )
set MM = Mx2Tran M;
set nV = n -VectSp_over F_Real;
set mV = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
A1: [#] (m -VectSp_over F_Real) = REAL m by MATRIX13:102
.= [#] (TOP-REAL m) by EUCLID:22 ;
A2: len Bm = m by Th19;
len Bn = n by Th19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by A2;
set T = Mx2Tran (M1,Bn,Bm);
A3: dom (Mx2Tran (M1,Bn,Bm)) = [#] (n -VectSp_over F_Real) by FUNCT_2:def 1;
A4: [#] (im (Mx2Tran (M1,Bn,Bm))) = (Mx2Tran (M1,Bn,Bm)) .: ([#] (n -VectSp_over F_Real)) by RANKNULL:def 2
.= rng (Mx2Tran (M1,Bn,Bm)) by A3, RELAT_1:113 ;
A5: Mx2Tran M = Mx2Tran (M1,Bn,Bm) by Th20;

hereby :: thesis: ( the_rank_of M = m implies Mx2Tran M is onto )

assume Mx2Tran M is onto ; :: thesis: the_rank_of M = m
then [#] (im (Mx2Tran (M1,Bn,Bm))) = [#] ((Omega). (m -VectSp_over F_Real)) by A5, A1, A4, FUNCT_2:def 3;
then rank (Mx2Tran (M1,Bn,Bm)) = dim ((Omega). (m -VectSp_over F_Real)) by VECTSP_4:29
.= m by MATRIX13:112 ;
hence the_rank_of M = m by MATRLIN2:49; :: thesis: verum

end;

A6: dim (m -VectSp_over F_Real) = m by MATRIX13:112;
assume the_rank_of M = m ; :: thesis: Mx2Tran M is onto
then m = rank (Mx2Tran (M1,Bn,Bm)) by MATRLIN2:49
.= dim (im (Mx2Tran (M1,Bn,Bm))) ;
then (Omega). (im (Mx2Tran (M1,Bn,Bm))) = (Omega). (m -VectSp_over F_Real) by A6, VECTSP_9:28;
hence Mx2Tran M is onto by A5, A1, A4, FUNCT_2:def 3; :: thesis: verum