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 ;
len Bn = n by Th19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by Th19;
set T = Mx2Tran (M1,Bn,Bm);
A2: dom (Mx2Tran (M1,Bn,Bm)) = [#] (n -VectSp_over F_Real) by FUNCT_2:def 1;
A3: [#] (im (Mx2Tran (M1,Bn,Bm))) = (Mx2Tran (M1,Bn,Bm)) .: ([#] (n -VectSp_over F_Real)) by RANKNULL:def 2
.= rng (Mx2Tran (M1,Bn,Bm)) by A2, RELAT_1:113 ;
A4: 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 A4, A1, A3, 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;

A5: 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 A5, VECTSP_9:28;
hence Mx2Tran M is onto by A4, A1, A3, FUNCT_2:def 3; :: thesis: verum