let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st the_rank_of A = len b1 holds
Mx2Tran (A,b1,b2) is one-to-one
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st the_rank_of A = len b1 holds
Mx2Tran (A,b1,b2) is one-to-one
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st the_rank_of A = len b1 holds
Mx2Tran (A,b1,b2) is one-to-one
let b2 be OrdBasis of V2; :: thesis: for A being Matrix of len b1, len b2,K st the_rank_of A = len b1 holds
Mx2Tran (A,b1,b2) is one-to-one
let A be Matrix of len b1, len b2,K; :: thesis: ( the_rank_of A = len b1 implies Mx2Tran (A,b1,b2) is one-to-one )
assume A1: the_rank_of A = len b1 ; :: thesis: Mx2Tran (A,b1,b2) is one-to-one
set S = Space_of_Solutions_of (A @);
set M = Mx2Tran (A,b1,b2);

A2: now :: thesis: the carrier of (ker (Mx2Tran (A,b1,b2))) c= {(0. V1)}

per cases ( len b1 = 0 or len b1 > 0 ) ;

suppose len b1 = 0 ; :: thesis: the carrier of (ker (Mx2Tran (A,b1,b2))) c= {(0. V1)}

then dim V1 = 0 by Th21;
then A3: (Omega). V1 = (0). V1 by VECTSP_9:29;
the carrier of (ker (Mx2Tran (A,b1,b2))) c= the carrier of V1 by VECTSP_4:def 2;
hence the carrier of (ker (Mx2Tran (A,b1,b2))) c= {(0. V1)} by A3, VECTSP_4:def 3; :: thesis: verum

end;

suppose A4: len b1 > 0 ; :: thesis: the carrier of (ker (Mx2Tran (A,b1,b2))) c= {(0. V1)}

A5: len b1 <= width A by A1, MATRIX13:74;
then A6: width (A @) = len A by A4, MATRIX_0:54;
A7: len A = len b1 by A4, MATRIX_0:23;
A8: width A = len b2 by A4, MATRIX_0:23;
thus the carrier of (ker (Mx2Tran (A,b1,b2))) c= {(0. V1)} :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ker (Mx2Tran (A,b1,b2))) or x in {(0. V1)} )
assume A9: x in the carrier of (ker (Mx2Tran (A,b1,b2))) ; :: thesis: x in {(0. V1)}
the carrier of (ker (Mx2Tran (A,b1,b2))) c= the carrier of V1 by VECTSP_4:def 2;
then reconsider v = x as Element of V1 by A9;
dim (Space_of_Solutions_of (A @)) = (len b1) - (the_rank_of (A @)) by A4, A7, A6, MATRIX15:68
.= (len b1) - (len b1) by A1, MATRIX13:84
.= 0 ;
then A10: (Omega). (Space_of_Solutions_of (A @)) = (0). (Space_of_Solutions_of (A @)) by VECTSP_9:29;
v in ker (Mx2Tran (A,b1,b2)) by A9;
then v |-- b1 in Space_of_Solutions_of (A @) by A4, A8, A5, Th41;
then v |-- b1 in the carrier of ((0). (Space_of_Solutions_of (A @))) by A10;
then v |-- b1 in the carrier of ((0). ((len b1) -VectSp_over K)) by A7, A6, VECTSP_4:36;
then v |-- b1 in {(0. ((len b1) -VectSp_over K))} by VECTSP_4:def 3;
then v |-- b1 = 0. ((len b1) -VectSp_over K) by TARSKI:def 1
.= (len b1) |-> (0. K) by MATRIX13:102
.= (0. V1) |-- b1 by Th20 ;
then v = 0. V1 by MATRLIN:34;
hence x in {(0. V1)} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

0. V1 in ker (Mx2Tran (A,b1,b2)) by RANKNULL:11;
then 0. V1 in the carrier of (ker (Mx2Tran (A,b1,b2))) ;
then {(0. V1)} c= the carrier of (ker (Mx2Tran (A,b1,b2))) by ZFMISC_1:31;
then the carrier of (ker (Mx2Tran (A,b1,b2))) = {(0. V1)} by A2, XBOOLE_0:def 10
.= the carrier of ((0). V1) by VECTSP_4:def 3 ;
then ker (Mx2Tran (A,b1,b2)) = (0). V1 by VECTSP_4:29;
hence Mx2Tran (A,b1,b2) is one-to-one by Th43; :: thesis: verum