let K be Field; :: thesis: for A, B being Matrix of K st len A = len B & ( width A = 0 implies width B = 0 ) holds
( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
let A, B be Matrix of K; :: thesis: ( len A = len B & ( width A = 0 implies width B = 0 ) implies ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty ) )
assume that
A1: len A = len B and
A2: ( width A = 0 implies width B = 0 ) ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
set wB = width B;
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by A1, MATRIX_0:51;
set wA = width A;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
deffunc H₁( Matrix of len A, width B,K, Nat, Nat, Element of K) -> FinSequence of the carrier of K * = RLine ($1,$2,((Line ($1,$2)) + ($4 * (Line ($1,$3)))));
defpred S₁[ set , set ] means for A1 being Matrix of len A, width A,K
for B1 being Matrix of len A, width B,K st A1 = $1 & B1 = $2 holds
( the_rank_of (A9 ^^ B9) = the_rank_of (A1 ^^ B1) & Solutions_of (A9,B9) = Solutions_of (A1,B1) );
A3: for A1 being Matrix of len A, width A,K
for B1 being Matrix of len A, width B,K st S₁[A1,B1] holds
for a being Element of K
for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S₁[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H₁(B1,i,j,a)] A14: S₁[A9,B9] ;
consider A1 being Matrix of len A, width A,K, B1 being Matrix of len A, width B,K, N being finite without_zero Subset of NAT such that
A15: N c= Seg (width A) and
A16: ( the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N ) and
A17: ( S₁[A1,B1] & Segm (A1,(Seg (card N)),N) = 1. (K,(card N)) ) and
A18: for i being Nat st i in dom A1 & i > card N holds
Line (A1,i) = (width A) |-> (0. K) and
for i, j being Nat st i in Seg (card N) & j in Seg (width A1) & j < (Sgm N) . i holds
A1 * (i,j) = 0. K from MATRIX15:sch 2(A14, A3);