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 len b1 > 0 & len b2 > 0 holds
nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)
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 len b1 > 0 & len b2 > 0 holds
nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)
let b2 be OrdBasis of V2; :: thesis: for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)
set I = id V1;
reconsider BB = MX2FinS (1. K,(len b1)) as OrdBasis of (len b1) -VectSp_over K by Th45;
let A be Matrix of len b1, len b2,K; :: thesis: ( len b1 > 0 & len b2 > 0 implies nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A) )
assume that
A1: len b1 > 0 and
A2: len b2 > 0 ; :: thesis: nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)
len BB = dim ((len b1) -VectSp_over K) by Th21
.= len b1 by MATRIX13:112 ;
then reconsider AI = AutMt (id V1),b1,b1 as Matrix of len b1, len BB,K ;
A3: ( AutMt (id V1),b1,b1 = 1. K,(len b1) & 0. K <> 1_ K ) by Th28;
(len b1) + 0 > 0 by A1;
then len b1 >= 1 by NAT_1:19;
then Det (1. K,(len b1)) = 1_ K by MATRIX_7:16;
then A4: the_rank_of AI = len b1 by A3, MATRIX13:83;
set S = Space_of_Solutions_of (A @ );
set KER = ker (Mx2Tran A,b1,b2);
set MAI = Mx2Tran AI,b1,BB;
set MK = (Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2));
A5: dom ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) = the carrier of (ker (Mx2Tran A,b1,b2)) by FUNCT_2:def 1;
A6: the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) c= the carrier of (Space_of_Solutions_of (A @ ))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) or x in the carrier of (Space_of_Solutions_of (A @ )) )
assume A7: x in the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) ; :: thesis: x in the carrier of (Space_of_Solutions_of (A @ ))
the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) c= the carrier of ((len b1) -VectSp_over K) by VECTSP_4:def 2;
then reconsider v = x as Element of ((len b1) -VectSp_over K) by A7;
v in im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) by A7, STRUCT_0:def 5;
then consider w being Element of (ker (Mx2Tran A,b1,b2)) such that
A8: v = ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) . w by RANKNULL:13;
A9: w in ker (Mx2Tran A,b1,b2) by STRUCT_0:def 5;
then w in V1 by VECTSP_4:17;
then reconsider W = w as Vector of V1 by STRUCT_0:def 5;
((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) . w = (Mx2Tran AI,b1,BB) . w by A5, FUNCT_1:70
.= ((id V1) . W) |-- b1 by Th47
.= W |-- b1 by FUNCT_1:34 ;
then ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) . w in Space_of_Solutions_of (A @ ) by A1, A2, A9, Th41;
hence x in the carrier of (Space_of_Solutions_of (A @ )) by A8, STRUCT_0:def 5; :: thesis: verum

end;

( len A = len b1 & width A = len b2 ) by A1, MATRIX_1:24;
then A10: width (A @ ) = len b1 by A2, MATRIX_2:12;
B2: Mx2Tran AI,b1,BB is one-to-one by A4, Th44;
dim ((len b1) -VectSp_over K) = len b1 by MATRIX13:112
.= dim V1 by Th21
.= rank (Mx2Tran AI,b1,BB) by RANKNULL:45, B2
.= dim (im (Mx2Tran AI,b1,BB)) ;
then A11: (Omega). ((len b1) -VectSp_over K) = (Omega). (im (Mx2Tran AI,b1,BB)) by VECTSP_9:32;
the carrier of (Space_of_Solutions_of (A @ )) c= the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Space_of_Solutions_of (A @ )) or x in the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) )
assume A12: x in the carrier of (Space_of_Solutions_of (A @ )) ; :: thesis: x in the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))))
the carrier of (Space_of_Solutions_of (A @ )) c= the carrier of ((len b1) -VectSp_over K) by A10, VECTSP_4:def 2;
then reconsider v = x as Element of ((len b1) -VectSp_over K) by A12;
A13: v in Space_of_Solutions_of (A @ ) by A12, STRUCT_0:def 5;
v in im (Mx2Tran AI,b1,BB) by A11, STRUCT_0:def 5;
then consider w being Element of V1 such that
A14: v = (Mx2Tran AI,b1,BB) . w by RANKNULL:13;
(Mx2Tran AI,b1,BB) . w = ((id V1) . w) |-- b1 by Th47
.= w |-- b1 by FUNCT_1:34 ;
then w in ker (Mx2Tran A,b1,b2) by A1, A2, A14, A13, Th41;
then reconsider W = w as Element of (ker (Mx2Tran A,b1,b2)) by STRUCT_0:def 5;
v = ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) . W by A5, A14, FUNCT_1:70;
then v in im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) by RANKNULL:13;
hence x in the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) by STRUCT_0:def 5; :: thesis: verum

end;

then the carrier of (Space_of_Solutions_of (A @ )) = the carrier of (im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)))) by A6, XBOOLE_0:def 10;
then A15: im ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) = Space_of_Solutions_of (A @ ) by A10, VECTSP_4:37;
Mx2Tran AI,b1,BB is one-to-one by A4, Th44;
then (Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2)) is one-to-one by FUNCT_1:84;
hence nullity (Mx2Tran A,b1,b2) = rank ((Mx2Tran AI,b1,BB) | (ker (Mx2Tran A,b1,b2))) by RANKNULL:45
.= (len b1) - (the_rank_of (A @ )) by A1, A10, A15, MATRIX15:68
.= (len b1) - (the_rank_of A) by MATRIX13:84 ;
:: thesis: verum
set M = Mx2Tran A,b1,b2;