let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real holds
( Mx2Tran M is one-to-one iff the_rank_of M = n )
let M be Matrix of n,m,F_Real; :: thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
set MM = Mx2Tran M;

per cases ( ( n = 0 iff m = 0 ) or ( n = 0 & m <> 0 ) or ( n <> 0 & m = 0 ) ) ;

suppose A1: ( n = 0 iff m = 0 ) ; :: thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )

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;
A2: len Bm = m by Th19;
A3: len Bn = n by Th19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by A2;
A4: len M1 = n by A1, MATRIX13:1;
A5: len Bm = m by Th19;
set T = Mx2Tran (M1,Bn,Bm);
A6: ( Mx2Tran (M1,Bn,Bm) is one-to-one iff ker (Mx2Tran (M1,Bn,Bm)) = (0). (n -VectSp_over F_Real) ) by MATRLIN2:43;
A7: width M1 = m by A1, MATRIX13:1;

per cases ( m = 0 or m > 0 ) ;

suppose A8: m = 0 ; :: thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )

A9: the carrier of (TOP-REAL 0) = {(0. (TOP-REAL 0))} by EUCLID:22, EUCLID:77;
then rng (Mx2Tran M) c= {(0. (TOP-REAL 0))} by A8, RELAT_1:def 19;
then rng (Mx2Tran M) = {(0. (TOP-REAL 0))} by ZFMISC_1:33;
then ( card {(0. (TOP-REAL 0))} = card {(0. (TOP-REAL 0))} & Mx2Tran M is onto ) by A8, A9, FUNCT_2:def 3;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A1, A4, A8, A9, MATRIX13:74, FINSEQ_4:63; :: thesis: verum

end;

suppose A10: m > 0 ; :: thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )

then reconsider SS = Space_of_Solutions_of (M1 @) as Subspace of n -VectSp_over F_Real by A4, A7, MATRIX_0:54;
A11: width (M1 @) = n by A4, A7, A10, MATRIX_0:54;

hereby :: thesis: ( the_rank_of M = n implies Mx2Tran M is one-to-one )

assume A12: Mx2Tran M is one-to-one ; :: thesis: the_rank_of M = n
[#] SS c= {(0. (n -VectSp_over F_Real))}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] SS or x in {(0. (n -VectSp_over F_Real))} )
assume A13: x in [#] SS ; :: thesis: x in {(0. (n -VectSp_over F_Real))}
then reconsider v = x as Vector of (n -VectSp_over F_Real) by VECTSP_4:10;
v = v |-- Bn by A3, MATRLIN2:46;
then v |-- Bn in SS by A13;
then v in ker (Mx2Tran (M1,Bn,Bm)) by A1, A3, A5, A10, MATRLIN2:41;
then v = 0. (n -VectSp_over F_Real) by A6, A12, Th20, VECTSP_4:35;
hence x in {(0. (n -VectSp_over F_Real))} by TARSKI:def 1; :: thesis: verum

end;

then [#] SS = {(0. (n -VectSp_over F_Real))} by ZFMISC_1:33;
then SS = (0). (n -VectSp_over F_Real) by VECTSP_4:def 3;
then dim SS = 0 by RANKNULL:16;
then 0 = n - (the_rank_of (M1 @)) by A1, A10, A11, MATRIX15:68;
hence the_rank_of M = n by MATRIX13:84; :: thesis: verum

end;

A14: the_rank_of (M1 @) = the_rank_of M by MATRIX13:84;
assume the_rank_of M = n ; :: thesis: Mx2Tran M is one-to-one
then dim SS = n - n by A1, A10, A11, A14, MATRIX15:68;
then A15: SS is trivial by MATRLIN2:42;
[#] (ker (Mx2Tran (M1,Bn,Bm))) c= {(0. (n -VectSp_over F_Real))}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (ker (Mx2Tran (M1,Bn,Bm))) or x in {(0. (n -VectSp_over F_Real))} )
assume A16: x in [#] (ker (Mx2Tran (M1,Bn,Bm))) ; :: thesis: x in {(0. (n -VectSp_over F_Real))}
then reconsider v = x as Vector of (n -VectSp_over F_Real) by VECTSP_4:10;
v in ker (Mx2Tran (M1,Bn,Bm)) by A16;
then v |-- Bn in SS by A1, A3, A5, A10, MATRLIN2:41;
then v in SS by A3, MATRLIN2:46;
then v in the carrier of SS ;
then v = 0. SS by A15;
then v = 0. (n -VectSp_over F_Real) by VECTSP_4:11;
hence x in {(0. (n -VectSp_over F_Real))} by TARSKI:def 1; :: thesis: verum

end;

then [#] (ker (Mx2Tran (M1,Bn,Bm))) = {(0. (n -VectSp_over F_Real))} by ZFMISC_1:33;
hence Mx2Tran M is one-to-one by A6, Th20, VECTSP_4:def 3; :: thesis: verum

end;

end;

end;

suppose A17: ( n = 0 & m <> 0 ) ; :: thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )

A18: now :: thesis: for x1, x2 being object st x1 in dom (Mx2Tran M) & x2 in dom (Mx2Tran M) & (Mx2Tran M) . x1 = (Mx2Tran M) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (Mx2Tran M) & x2 in dom (Mx2Tran M) & (Mx2Tran M) . x1 = (Mx2Tran M) . x2 implies x1 = x2 )
assume A19: ( x1 in dom (Mx2Tran M) & x2 in dom (Mx2Tran M) & (Mx2Tran M) . x1 = (Mx2Tran M) . x2 ) ; :: thesis: x1 = x2
A20: dom (Mx2Tran M) = [#] (TOP-REAL 0) by A17, FUNCT_2:def 1
.= {(0. (TOP-REAL 0))} by EUCLID:22, EUCLID:77 ;
hence x1 = 0. (TOP-REAL 0) by A19, TARSKI:def 1
.= x2 by A19, A20, TARSKI:def 1 ;
:: thesis: verum

end;

len M = n by MATRIX_0:def 2;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A18, A17, FUNCT_1:def 4, MATRIX13:74; :: thesis: verum

end;

suppose A21: ( n <> 0 & m = 0 ) ; :: thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )

reconsider x1 = n |-> 1 as Point of (TOP-REAL n) by Lm2;
reconsider x2 = n |-> 2 as Point of (TOP-REAL n) by Lm2;
A22: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
A23: (Mx2Tran M) . x1 = 0. (TOP-REAL 0) by A21
.= (Mx2Tran M) . x2 by A21 ;
A24: x1 <> x2

proof

assume A25: x1 = x2 ; :: thesis: contradiction
A26: x1 = (Seg n) --> 1 by FINSEQ_2:def 2
.= [:(Seg n),{1}:] by FUNCOP_1:def 2 ;
x2 = (Seg n) --> 2 by FINSEQ_2:def 2
.= [:(Seg n),{2}:] by FUNCOP_1:def 2 ;
then {1} = {2} by A25, A26, A21, ZFMISC_1:110;
then 2 in {1} by TARSKI:def 1;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

width M = m by A21, MATRIX13:1;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A24, A21, A23, A22, FUNCT_1:def 4, MATRIX13:74; :: thesis: verum

end;

end;