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:9;
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:47
.= ((id V1) . W) |-- b1 by Th47
.= W |-- b1 by FUNCT_1:17 ;
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:23;
then A10: width (A @) = len b1 by A2, MATRIX_2:10;
A11: 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 A11, RANKNULL:45
.= dim (im (Mx2Tran (AI,b1,BB))) ;
then A12: (Omega). ((len b1) -VectSp_over K) = (Omega). (im (Mx2Tran (AI,b1,BB))) by VECTSP_9:28;
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 A13: 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 A13;
A14: v in Space_of_Solutions_of (A @) by A13, STRUCT_0:def 5;
v in im (Mx2Tran (AI,b1,BB)) by A12, STRUCT_0:def 5;
then consider w being Element of V1 such that
A15: 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:17 ;
then w in ker (Mx2Tran (A,b1,b2)) by A1, A2, A15, A14, 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, A15, FUNCT_1:47;
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 A16: im ((Mx2Tran (AI,b1,BB)) | (ker (Mx2Tran (A,b1,b2)))) = Space_of_Solutions_of (A @) by A10, VECTSP_4:29;
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:52;
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, A16, MATRIX15:68
.= (len b1) - (the_rank_of A) by MATRIX13:84 ;
:: thesis: verum