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 M = Mx2Tran A,b1,b2;
set S = Space_of_Solutions_of (A @ );

A2: now

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 ( (Omega). V1 = (0). V1 & the carrier of (ker (Mx2Tran A,b1,b2)) c= the carrier of V1 & the carrier of ((0). V1) = {(0. V1)} ) by VECTSP_4:def 2, VECTSP_4:def 3, VECTSP_9:33;
hence the carrier of (ker (Mx2Tran A,b1,b2)) c= {(0. V1)} ; :: thesis: verum

end;

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

then A4: ( len A = len b1 & width A = len b2 & len b1 <= width A ) by A1, MATRIX13:74, MATRIX_1:24;
A5: width (A @ ) = len A by A3, A4, MATRIX_2:12;
thus the carrier of (ker (Mx2Tran A,b1,b2)) c= {(0. V1)} :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ker (Mx2Tran A,b1,b2)) or x in {(0. V1)} )
assume A6: 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 A6;
dim (Space_of_Solutions_of (A @ )) = (len b1) - (the_rank_of (A @ )) by A3, A4, A5, MATRIX15:68
.= (len b1) - (len b1) by A1, MATRIX13:84
.= 0 ;
then A7: (Omega). (Space_of_Solutions_of (A @ )) = (0). (Space_of_Solutions_of (A @ )) by VECTSP_9:33;
v in ker (Mx2Tran A,b1,b2) by A6, STRUCT_0:def 5;
then v |-- b1 in Space_of_Solutions_of (A @ ) by Th41, A3, A4;
then v |-- b1 in the carrier of ((0). (Space_of_Solutions_of (A @ ))) by A7, STRUCT_0:def 5;
then v |-- b1 in the carrier of ((0). ((len b1) -VectSp_over K)) by A4, A5, VECTSP_4:47;
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:39;
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)) by STRUCT_0:def 5;
then {(0. V1)} c= the carrier of (ker (Mx2Tran A,b1,b2)) by ZFMISC_1:37;
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:37;
hence Mx2Tran A,b1,b2 is one-to-one by Th43; :: thesis: verum