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

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

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

A8: the carrier of (TOP-REAL 0) = {(0. (TOP-REAL 0))} by EUCLID:22, JORDAN2C:105;
then rng (Mx2Tran M) c= {(0. (TOP-REAL 0))} by A7, 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 A7, A8, FUNCT_2:def 3;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A1, A3, A7, A8, MATRIX13:74, STIRL2_1:60; :: thesis: verum

end;

suppose A9: 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 A3, A6, MATRIX_2:10;
A10: width (M1 @) = n by A3, A6, A9, MATRIX_2:10;

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

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] SS or x in {(0. (n -VectSp_over F_Real))} )
assume A12: 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 A2, MATRLIN2:46;
then v |-- Bn in SS by A12, STRUCT_0:def 5;
then v in ker (Mx2Tran (M1,Bn,Bm)) by A1, A2, A4, A9, MATRLIN2:41;
then v = 0. (n -VectSp_over F_Real) by A5, A11, 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, A9, A10, MATRIX15:68;
hence the_rank_of M = n by MATRIX13:84; :: thesis: verum

end;

A13: 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, A9, A10, A13, MATRIX15:68;
then A14: SS is trivial by MATRLIN2:42;
[#] (ker (Mx2Tran (M1,Bn,Bm))) c= {(0. (n -VectSp_over F_Real))}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (ker (Mx2Tran (M1,Bn,Bm))) or x in {(0. (n -VectSp_over F_Real))} )
assume A15: 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 A15, STRUCT_0:def 5;
then v |-- Bn in SS by A1, A2, A4, A9, MATRLIN2:41;
then v in SS by A2, MATRLIN2:46;
then v in the carrier of SS by STRUCT_0:def 5;
then v = 0. SS by A14, STRUCT_0:def 18;
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 A5, Th20, VECTSP_4:def 3; :: thesis: verum

end;

end;

end;

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

A17: now

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

end;

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

end;

suppose A20: ( 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;
A21: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
A22: (Mx2Tran M) . x1 = 0. (TOP-REAL 0) by A20
.= (Mx2Tran M) . x2 by A20 ;
A23: x1 <> x2

proof

assume A24: x1 = x2 ; :: thesis: contradiction
A25: 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 A24, A25, A20, ZFMISC_1:110;
then 2 in {1} by TARSKI:def 1;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

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

end;

end;