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_{1}( 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_{1}[ 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_{1}[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_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]
_{1}[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_{1}[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);

( 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

defpred S

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

for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

proof

A14:
S
let A1 be Matrix of len A, width A,K; :: thesis: for B1 being Matrix of len A, width B,K st S_{1}[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_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

let B1 be Matrix of len A, width B,K; :: thesis: ( S_{1}[A1,B1] implies for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)] )

assume A4: S_{1}[A1,B1]
; :: thesis: for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

let a be Element of K; :: thesis: for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)] )

assume that

A5: j in dom A1 and

A6: ( i = j implies a <> - (1_ K) ) ; :: thesis: S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

set LAj = Line (A1,j);

set LAi = Line (A1,i);

set RA = RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))));

A7: dom A1 = Seg (len A1) by FINSEQ_1:def 3

.= Seg (len A) by MATRIX_0:def 2 ;

then A8: Solutions_of (A1,B1) = Solutions_of ((RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))),H_{1}(B1,i,j,a))
by A5, A6, Th40;

set RB = H_{1}(B1,i,j,a);

set LBj = Line (B1,j);

set LBi = Line (B1,i);

A9: ( len A1 = len A & len B1 = len A ) by MATRIX_0:def 2;

end;for a being Element of K

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

let B1 be Matrix of len A, width B,K; :: thesis: ( S

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

assume A4: S

for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

let a be Element of K; :: thesis: for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds

S

let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S

assume that

A5: j in dom A1 and

A6: ( i = j implies a <> - (1_ K) ) ; :: thesis: S

set LAj = Line (A1,j);

set LAi = Line (A1,i);

set RA = RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))));

A7: dom A1 = Seg (len A1) by FINSEQ_1:def 3

.= Seg (len A) by MATRIX_0:def 2 ;

then A8: Solutions_of (A1,B1) = Solutions_of ((RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))),H

set RB = H

set LBj = Line (B1,j);

set LBi = Line (B1,i);

A9: ( len A1 = len A & len B1 = len A ) by MATRIX_0:def 2;

per cases
( not i in Seg (len A) or i in Seg (len A) )
;

end;

suppose
not i in Seg (len A)
; :: thesis: S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

then
( RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))) = A1 & H_{1}(B1,i,j,a) = B1 )
by A9, MATRIX13:40;

hence S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]
by A4; :: thesis: verum

end;hence S

suppose A10:
i in Seg (len A)
; :: thesis: S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]

A11:
len (A1 ^^ B1) = len A
by MATRIX_0:def 2;

A12: ( len (a * (Line (A1,j))) = width A1 & len (a * (Line (B1,j))) = width B1 ) by CARD_1:def 7;

A13: ( len (Line (A1,i)) = width A1 & len (Line (B1,i)) = width B1 ) by CARD_1:def 7;

( len ((Line (A1,i)) + (a * (Line (A1,j)))) = width A1 & len ((Line (B1,i)) + (a * (Line (B1,j)))) = width B1 ) by CARD_1:def 7;

then (RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) ^^ H_{1}(B1,i,j,a) =
RLine ((A1 ^^ B1),i,(((Line (A1,i)) + (a * (Line (A1,j)))) ^ ((Line (B1,i)) + (a * (Line (B1,j))))))
by Th18

.= RLine ((A1 ^^ B1),i,(((Line (A1,i)) ^ (Line (B1,i))) + ((a * (Line (A1,j))) ^ (a * (Line (B1,j)))))) by A13, A12, Th3

.= RLine ((A1 ^^ B1),i,(((Line (A1,i)) ^ (Line (B1,i))) + (a * ((Line (A1,j)) ^ (Line (B1,j)))))) by Th4

.= RLine ((A1 ^^ B1),i,((Line ((A1 ^^ B1),i)) + (a * ((Line (A1,j)) ^ (Line (B1,j)))))) by A10, Th15

.= RLine ((A1 ^^ B1),i,((Line ((A1 ^^ B1),i)) + (a * (Line ((A1 ^^ B1),j))))) by A5, A7, Th15 ;

then the_rank_of ((RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) ^^ H_{1}(B1,i,j,a)) = the_rank_of (A1 ^^ B1)
by A5, A6, A7, A11, MATRIX13:92;

hence S_{1}[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H_{1}(B1,i,j,a)]
by A4, A8; :: thesis: verum

end;A12: ( len (a * (Line (A1,j))) = width A1 & len (a * (Line (B1,j))) = width B1 ) by CARD_1:def 7;

A13: ( len (Line (A1,i)) = width A1 & len (Line (B1,i)) = width B1 ) by CARD_1:def 7;

( len ((Line (A1,i)) + (a * (Line (A1,j)))) = width A1 & len ((Line (B1,i)) + (a * (Line (B1,j)))) = width B1 ) by CARD_1:def 7;

then (RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) ^^ H

.= RLine ((A1 ^^ B1),i,(((Line (A1,i)) ^ (Line (B1,i))) + ((a * (Line (A1,j))) ^ (a * (Line (B1,j)))))) by A13, A12, Th3

.= RLine ((A1 ^^ B1),i,(((Line (A1,i)) ^ (Line (B1,i))) + (a * ((Line (A1,j)) ^ (Line (B1,j)))))) by Th4

.= RLine ((A1 ^^ B1),i,((Line ((A1 ^^ B1),i)) + (a * ((Line (A1,j)) ^ (Line (B1,j)))))) by A10, Th15

.= RLine ((A1 ^^ B1),i,((Line ((A1 ^^ B1),i)) + (a * (Line ((A1 ^^ B1),j))))) by A5, A7, Th15 ;

then the_rank_of ((RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) ^^ H

hence S

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

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);

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

end;

suppose A19:
len A = 0
; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )

then
( len (A9 ^^ B9) = 0 & the_rank_of A = 0 )
by MATRIX13:74, MATRIX_0:def 2;

hence ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty ) by A19, Th51, MATRIX13:74; :: thesis: verum

end;hence ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty ) by A19, Th51, MATRIX13:74; :: thesis: verum

suppose A20:
len A > 0
; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )

end;

per cases
( N <> {} or N = {} )
;

end;

suppose A21:
N <> {}
; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )

set SN = Seg (card N);

set SS = (Seg (len A)) \ (Seg (card N));

A22: card (Seg (card N)) = card N by FINSEQ_1:57;

reconsider P2 = (Sgm (Seg (card N))) " (Seg (card N)), Q2 = (Sgm (Seg (width A))) " N as finite without_zero Subset of NAT by MATRIX13:53;

( dom (Sgm (Seg (card N))) = Seg (card (Seg (card N))) & rng (Sgm (Seg (card N))) = Seg (card N) ) by FINSEQ_1:def 13, FINSEQ_3:40;

then A23: P2 = Seg (card N) by A22, RELAT_1:134;

rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 13;

then A24: (Sgm (Seg (width A))) .: Q2 = N by A15, FUNCT_1:77;

( Q2 c= dom (Sgm (Seg (width A))) & Sgm (Seg (width A)) is one-to-one ) by FINSEQ_3:92, RELAT_1:132;

then N,Q2 are_equipotent by A24, CARD_1:33;

then A25: ( dom (Sgm (Seg (width A))) = Seg (card (Seg (width A))) & card N = card Q2 ) by CARD_1:5, FINSEQ_3:40;

A26: ( Seg (len A1) = dom A1 & len A1 = len A ) by A20, FINSEQ_1:def 3, MATRIX_0:23;

A27: width A1 = width A by A20, MATRIX_0:23;

then A31: Seg (card N) c= Seg (len A) by FINSEQ_1:5;

A32: len B1 = len A by A20, MATRIX_0:23;

A33: ( Seg (len B1) = dom B1 & width B1 = width B ) by A20, FINSEQ_1:def 3, MATRIX_0:23;

thus ( the_rank_of A = the_rank_of (A ^^ B) implies not Solutions_of (A,B) is empty ) :: thesis: ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) )

thus ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum

end;set SS = (Seg (len A)) \ (Seg (card N));

A22: card (Seg (card N)) = card N by FINSEQ_1:57;

reconsider P2 = (Sgm (Seg (card N))) " (Seg (card N)), Q2 = (Sgm (Seg (width A))) " N as finite without_zero Subset of NAT by MATRIX13:53;

( dom (Sgm (Seg (card N))) = Seg (card (Seg (card N))) & rng (Sgm (Seg (card N))) = Seg (card N) ) by FINSEQ_1:def 13, FINSEQ_3:40;

then A23: P2 = Seg (card N) by A22, RELAT_1:134;

rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 13;

then A24: (Sgm (Seg (width A))) .: Q2 = N by A15, FUNCT_1:77;

( Q2 c= dom (Sgm (Seg (width A))) & Sgm (Seg (width A)) is one-to-one ) by FINSEQ_3:92, RELAT_1:132;

then N,Q2 are_equipotent by A24, CARD_1:33;

then A25: ( dom (Sgm (Seg (width A))) = Seg (card (Seg (width A))) & card N = card Q2 ) by CARD_1:5, FINSEQ_3:40;

A26: ( Seg (len A1) = dom A1 & len A1 = len A ) by A20, FINSEQ_1:def 3, MATRIX_0:23;

A27: width A1 = width A by A20, MATRIX_0:23;

A28: now :: thesis: for i being Nat st i in (Seg (len A)) \ (Seg (card N)) holds

Line (A1,i) = (width A1) |-> (0. K)

card N <= len A
by A16, MATRIX13:74;Line (A1,i) = (width A1) |-> (0. K)

let i be Nat; :: thesis: ( i in (Seg (len A)) \ (Seg (card N)) implies Line (A1,i) = (width A1) |-> (0. K) )

assume A29: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line (A1,i) = (width A1) |-> (0. K)

not i in Seg (card N) by A29, XBOOLE_0:def 5;

then A30: ( i < 1 or i > card N ) ;

i in Seg (len A) by A29, XBOOLE_0:def 5;

hence Line (A1,i) = (width A1) |-> (0. K) by A18, A26, A27, A30, FINSEQ_1:1; :: thesis: verum

end;assume A29: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line (A1,i) = (width A1) |-> (0. K)

not i in Seg (card N) by A29, XBOOLE_0:def 5;

then A30: ( i < 1 or i > card N ) ;

i in Seg (len A) by A29, XBOOLE_0:def 5;

hence Line (A1,i) = (width A1) |-> (0. K) by A18, A26, A27, A30, FINSEQ_1:1; :: thesis: verum

then A31: Seg (card N) c= Seg (len A) by FINSEQ_1:5;

A32: len B1 = len A by A20, MATRIX_0:23;

A33: ( Seg (len B1) = dom B1 & width B1 = width B ) by A20, FINSEQ_1:def 3, MATRIX_0:23;

thus ( the_rank_of A = the_rank_of (A ^^ B) implies not Solutions_of (A,B) is empty ) :: thesis: ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) )

proof

A35:
(Seg (len A)) \ (Seg (card N)) c= Seg (len A)
by XBOOLE_1:36;
assume
the_rank_of A = the_rank_of (A ^^ B)
; :: thesis: not Solutions_of (A,B) is empty

then the_rank_of A1 = the_rank_of (A1 ^^ B1) by A16, A17;

then for i being Nat st i in (dom A1) \ (Seg (card N)) holds

( Line (A1,i) = (width A1) |-> (0. K) & Line (B1,i) = (width B1) |-> (0. K) ) by A26, A32, A28, Th24, XBOOLE_1:36;

then A34: Solutions_of (A1,B1) = Solutions_of ((Segm (A1,(Seg (card N)),(Seg (width A)))),(Segm (B1,(Seg (card N)),(Seg (width B))))) by A21, A31, A26, A32, A27, A33, Th45;

Segm ((Segm (A1,(Seg (card N)),(Seg (width A)))),P2,Q2) = 1. (K,(card N)) by A15, A17, MATRIX13:56;

then ex X being Matrix of card (Seg (width A)), card (Seg (width B)),K st

( Segm (X,((Seg (card (Seg (width A)))) \ Q2),(Seg (card (Seg (width B))))) = 0. (K,((card (Seg (width A))) -' (card (Seg (card N)))),(card (Seg (width B)))) & Segm (X,Q2,(Seg (card (Seg (width B))))) = Segm (B1,(Seg (card N)),(Seg (width B))) & X in Solutions_of ((Segm (A1,(Seg (card N)),(Seg (width A)))),(Segm (B1,(Seg (card N)),(Seg (width B))))) ) by A21, A22, A23, A25, Th50, RELAT_1:132;

hence not Solutions_of (A,B) is empty by A17, A34; :: thesis: verum

end;then the_rank_of A1 = the_rank_of (A1 ^^ B1) by A16, A17;

then for i being Nat st i in (dom A1) \ (Seg (card N)) holds

( Line (A1,i) = (width A1) |-> (0. K) & Line (B1,i) = (width B1) |-> (0. K) ) by A26, A32, A28, Th24, XBOOLE_1:36;

then A34: Solutions_of (A1,B1) = Solutions_of ((Segm (A1,(Seg (card N)),(Seg (width A)))),(Segm (B1,(Seg (card N)),(Seg (width B))))) by A21, A31, A26, A32, A27, A33, Th45;

Segm ((Segm (A1,(Seg (card N)),(Seg (width A)))),P2,Q2) = 1. (K,(card N)) by A15, A17, MATRIX13:56;

then ex X being Matrix of card (Seg (width A)), card (Seg (width B)),K st

( Segm (X,((Seg (card (Seg (width A)))) \ Q2),(Seg (card (Seg (width B))))) = 0. (K,((card (Seg (width A))) -' (card (Seg (card N)))),(card (Seg (width B)))) & Segm (X,Q2,(Seg (card (Seg (width B))))) = Segm (B1,(Seg (card N)),(Seg (width B))) & X in Solutions_of ((Segm (A1,(Seg (card N)),(Seg (width A)))),(Segm (B1,(Seg (card N)),(Seg (width B))))) ) by A21, A22, A23, A25, Th50, RELAT_1:132;

hence not Solutions_of (A,B) is empty by A17, A34; :: thesis: verum

thus ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum

proof

assume
not Solutions_of (A,B) is empty
; :: thesis: the_rank_of A = the_rank_of (A ^^ B)

then not Solutions_of (A1,B1) is empty by A17;

then consider x being object such that

A36: x in Solutions_of (A1,B1) ;

set AB = A1 ^^ B1;

A37: len (Segm ((A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1))))) = card (Seg (card N)) by MATRIX_0:def 2;

A38: ( dom (A1 ^^ B1) = Seg (len (A1 ^^ B1)) & len (A1 ^^ B1) = len A ) by A20, FINSEQ_1:def 3, MATRIX_0:23;

reconsider x = x as Matrix of width A, width B,K by A20, A36, Th53;

A39: the_rank_of (Segm ((A1 ^^ B1),(Seg (len A)),(Seg (width A1)))) = card N by A16, Th19;

A40: width (A1 ^^ B1) = (width A1) + (width B1) by A20, MATRIX_0:23;

then the_rank_of (A1 ^^ B1) <= card (Seg (card N)) by A37, MATRIX13:74;

then A44: the_rank_of (A1 ^^ B1) <= card N by FINSEQ_1:57;

width A1 <= width (A1 ^^ B1) by A40, NAT_1:11;

then Seg (width A1) c= Seg (width (A1 ^^ B1)) by FINSEQ_1:5;

then [:(Seg (len A)),(Seg (width A1)):] c= Indices (A1 ^^ B1) by A38, ZFMISC_1:95;

then card N <= the_rank_of (A1 ^^ B1) by A39, MATRIX13:79;

then the_rank_of (A1 ^^ B1) = card N by A44, XXREAL_0:1;

hence the_rank_of A = the_rank_of (A ^^ B) by A16, A17; :: thesis: verum

end;then not Solutions_of (A1,B1) is empty by A17;

then consider x being object such that

A36: x in Solutions_of (A1,B1) ;

set AB = A1 ^^ B1;

A37: len (Segm ((A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1))))) = card (Seg (card N)) by MATRIX_0:def 2;

A38: ( dom (A1 ^^ B1) = Seg (len (A1 ^^ B1)) & len (A1 ^^ B1) = len A ) by A20, FINSEQ_1:def 3, MATRIX_0:23;

reconsider x = x as Matrix of width A, width B,K by A20, A36, Th53;

A39: the_rank_of (Segm ((A1 ^^ B1),(Seg (len A)),(Seg (width A1)))) = card N by A16, Th19;

A40: width (A1 ^^ B1) = (width A1) + (width B1) by A20, MATRIX_0:23;

now :: thesis: for i being Nat st i in (Seg (len A)) \ (Seg (card N)) holds

Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K)

then
the_rank_of (Segm ((A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1))))) = the_rank_of (A1 ^^ B1)
by A31, A38, Th11;Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K)

let i be Nat; :: thesis: ( i in (Seg (len A)) \ (Seg (card N)) implies Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K) )

assume A41: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K)

A42: Line (A1,i) = (width A1) |-> (0. K) by A28, A41;

A43: ( x in Solutions_of (A1,B1) & i in dom A1 & Line (A1,i) = (width A1) |-> (0. K) implies Line (B1,i) = (width B1) |-> (0. K) ) by Th41;

thus Line ((A1 ^^ B1),i) = (Line (A1,i)) ^ (Line (B1,i)) by A35, A41, Th15

.= (width (A1 ^^ B1)) |-> (0. K) by A26, A35, A36, A40, A41, A42, A43, FINSEQ_2:123 ; :: thesis: verum

end;assume A41: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K)

A42: Line (A1,i) = (width A1) |-> (0. K) by A28, A41;

A43: ( x in Solutions_of (A1,B1) & i in dom A1 & Line (A1,i) = (width A1) |-> (0. K) implies Line (B1,i) = (width B1) |-> (0. K) ) by Th41;

thus Line ((A1 ^^ B1),i) = (Line (A1,i)) ^ (Line (B1,i)) by A35, A41, Th15

.= (width (A1 ^^ B1)) |-> (0. K) by A26, A35, A36, A40, A41, A42, A43, FINSEQ_2:123 ; :: thesis: verum

then the_rank_of (A1 ^^ B1) <= card (Seg (card N)) by A37, MATRIX13:74;

then A44: the_rank_of (A1 ^^ B1) <= card N by FINSEQ_1:57;

width A1 <= width (A1 ^^ B1) by A40, NAT_1:11;

then Seg (width A1) c= Seg (width (A1 ^^ B1)) by FINSEQ_1:5;

then [:(Seg (len A)),(Seg (width A1)):] c= Indices (A1 ^^ B1) by A38, ZFMISC_1:95;

then card N <= the_rank_of (A1 ^^ B1) by A39, MATRIX13:79;

then the_rank_of (A1 ^^ B1) = card N by A44, XXREAL_0:1;

hence the_rank_of A = the_rank_of (A ^^ B) by A16, A17; :: thesis: verum

suppose A45:
N = {}
; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )

set ZERO = 0. (K,(len A),(width A));

A51: width A1 = width A by A20, MATRIX_0:23;

len A1 = len A by A20, MATRIX_0:23;

then 0. (K,(len A),(width A)) = A1 by A50, A46;

then A52: the_rank_of A = 0 by A16, A50, A51, MATRIX13:95;

then A53: 0. (K,(len A),(width A)) = A by MATRIX13:95;

A54: Indices (A9 ^^ B9) = [:(Seg (len A)),(Seg ((width A) + (width B))):] by A20, MATRIX_0:23;

thus ( the_rank_of A = the_rank_of (A ^^ B) implies not Solutions_of (A,B) is empty ) :: thesis: ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) )

A59: (width A) + (width B) = width (A9 ^^ B9) by A20, MATRIX_0:23;

A60: Indices (0. (K,(len A),(width A))) = [:(Seg (len A)),(Seg (width A)):] by A20, MATRIX_0:23;

thus ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum

end;A46: now :: thesis: for i being Nat st 1 <= i & i <= len A holds

(0. (K,(len A),(width A))) . i = A1 . i

A50:
len (0. (K,(len A),(width A))) = len A
by A20, MATRIX_0:23;(0. (K,(len A),(width A))) . i = A1 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len A implies (0. (K,(len A),(width A))) . i = A1 . i )

assume A47: ( 1 <= i & i <= len A ) ; :: thesis: (0. (K,(len A),(width A))) . i = A1 . i

A48: ( dom A1 = Seg (len A1) & len A1 = len A ) by FINSEQ_1:def 3, MATRIX_0:def 2;

A49: i in Seg (len A) by A47;

hence (0. (K,(len A),(width A))) . i = (width A) |-> (0. K) by FINSEQ_2:57

.= Line (A1,i) by A18, A45, A49, A48

.= A1 . i by A49, MATRIX_0:52 ;

:: thesis: verum

end;assume A47: ( 1 <= i & i <= len A ) ; :: thesis: (0. (K,(len A),(width A))) . i = A1 . i

A48: ( dom A1 = Seg (len A1) & len A1 = len A ) by FINSEQ_1:def 3, MATRIX_0:def 2;

A49: i in Seg (len A) by A47;

hence (0. (K,(len A),(width A))) . i = (width A) |-> (0. K) by FINSEQ_2:57

.= Line (A1,i) by A18, A45, A49, A48

.= A1 . i by A49, MATRIX_0:52 ;

:: thesis: verum

A51: width A1 = width A by A20, MATRIX_0:23;

len A1 = len A by A20, MATRIX_0:23;

then 0. (K,(len A),(width A)) = A1 by A50, A46;

then A52: the_rank_of A = 0 by A16, A50, A51, MATRIX13:95;

then A53: 0. (K,(len A),(width A)) = A by MATRIX13:95;

A54: Indices (A9 ^^ B9) = [:(Seg (len A)),(Seg ((width A) + (width B))):] by A20, MATRIX_0:23;

thus ( the_rank_of A = the_rank_of (A ^^ B) implies not Solutions_of (A,B) is empty ) :: thesis: ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) )

proof

A58:
Indices B9 = [:(Seg (len A)),(Seg (width B)):]
by A20, MATRIX_0:23;
set x = the Matrix of width A, width B,K;

assume A55: the_rank_of A = the_rank_of (A ^^ B) ; :: thesis: not Solutions_of (A,B) is empty

(Seg ((width A) + (width B))) \ (Seg (width A)) c= Seg ((width A) + (width B)) by XBOOLE_1:36;

then A56: [:(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A))):] c= Indices (A ^^ B) by A54, ZFMISC_1:95;

Segm ((A9 ^^ B9),(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B by Th19;

then 0 = the_rank_of B by A52, A55, A56, MATRIX13:79;

then A57: B = 0. (K,(len A),(width B)) by A1, MATRIX13:95;

then ( ( width A = 0 & width B = 0 ) or Solutions_of (A9,B9) = { X where X is Matrix of width A, width B,K : verum } ) by A2, A20, A53, Th54;

then ( Solutions_of (A9,B9) = {{}} or the Matrix of width A, width B,K in Solutions_of (A9,B9) ) by A53, A57, Th56;

hence not Solutions_of (A,B) is empty ; :: thesis: verum

end;assume A55: the_rank_of A = the_rank_of (A ^^ B) ; :: thesis: not Solutions_of (A,B) is empty

(Seg ((width A) + (width B))) \ (Seg (width A)) c= Seg ((width A) + (width B)) by XBOOLE_1:36;

then A56: [:(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A))):] c= Indices (A ^^ B) by A54, ZFMISC_1:95;

Segm ((A9 ^^ B9),(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B by Th19;

then 0 = the_rank_of B by A52, A55, A56, MATRIX13:79;

then A57: B = 0. (K,(len A),(width B)) by A1, MATRIX13:95;

then ( ( width A = 0 & width B = 0 ) or Solutions_of (A9,B9) = { X where X is Matrix of width A, width B,K : verum } ) by A2, A20, A53, Th54;

then ( Solutions_of (A9,B9) = {{}} or the Matrix of width A, width B,K in Solutions_of (A9,B9) ) by A53, A57, Th56;

hence not Solutions_of (A,B) is empty ; :: thesis: verum

A59: (width A) + (width B) = width (A9 ^^ B9) by A20, MATRIX_0:23;

A60: Indices (0. (K,(len A),(width A))) = [:(Seg (len A)),(Seg (width A)):] by A20, MATRIX_0:23;

thus ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum

proof

assume A61:
not Solutions_of (A,B) is empty
; :: thesis: the_rank_of A = the_rank_of (A ^^ B)

assume the_rank_of A <> the_rank_of (A ^^ B) ; :: thesis: contradiction

then consider i, j being Nat such that

A62: [i,j] in Indices (A9 ^^ B9) and

A63: (A9 ^^ B9) * (i,j) <> 0. K by A52, MATRIX13:94;

A64: j in Seg ((width A) + (width B)) by A59, A62, ZFMISC_1:87;

A65: dom (Line ((A9 ^^ B9),i)) = Seg ((width A) + (width B)) by A59, FINSEQ_2:124;

A66: len (Line (A9,i)) = width A by CARD_1:def 7;

A67: dom (Line (B9,i)) = Seg (width B) by FINSEQ_2:124;

A68: dom (Line (A9,i)) = Seg (width A) by FINSEQ_2:124;

A69: i in Seg (len A) by A54, A62, ZFMISC_1:87;

then A70: Line ((A9 ^^ B9),i) = (Line (A9,i)) ^ (Line (B9,i)) by Th15;

end;assume the_rank_of A <> the_rank_of (A ^^ B) ; :: thesis: contradiction

then consider i, j being Nat such that

A62: [i,j] in Indices (A9 ^^ B9) and

A63: (A9 ^^ B9) * (i,j) <> 0. K by A52, MATRIX13:94;

A64: j in Seg ((width A) + (width B)) by A59, A62, ZFMISC_1:87;

A65: dom (Line ((A9 ^^ B9),i)) = Seg ((width A) + (width B)) by A59, FINSEQ_2:124;

A66: len (Line (A9,i)) = width A by CARD_1:def 7;

A67: dom (Line (B9,i)) = Seg (width B) by FINSEQ_2:124;

A68: dom (Line (A9,i)) = Seg (width A) by FINSEQ_2:124;

A69: i in Seg (len A) by A54, A62, ZFMISC_1:87;

then A70: Line ((A9 ^^ B9),i) = (Line (A9,i)) ^ (Line (B9,i)) by Th15;

per cases
( j in dom (Line (A9,i)) or ex n being Nat st

( n in dom (Line (B9,i)) & j = (width A) + n ) ) by A64, A66, A65, A70, FINSEQ_1:25;

end;

( n in dom (Line (B9,i)) & j = (width A) + n ) ) by A64, A66, A65, A70, FINSEQ_1:25;

suppose A71:
j in dom (Line (A9,i))
; :: thesis: contradiction

then A72:
[i,j] in Indices (0. (K,(len A),(width A)))
by A60, A69, A68, ZFMISC_1:87;

(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by A59, A64, MATRIX_0:def 7

.= (Line (A9,i)) . j by A70, A71, FINSEQ_1:def 7

.= A9 * (i,j) by A68, A71, MATRIX_0:def 7

.= 0. K by A53, A72, MATRIX_3:1 ;

hence contradiction by A63; :: thesis: verum

end;(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by A59, A64, MATRIX_0:def 7

.= (Line (A9,i)) . j by A70, A71, FINSEQ_1:def 7

.= A9 * (i,j) by A68, A71, MATRIX_0:def 7

.= 0. K by A53, A72, MATRIX_3:1 ;

hence contradiction by A63; :: thesis: verum

suppose
ex n being Nat st

( n in dom (Line (B9,i)) & j = (width A) + n ) ; :: thesis: contradiction

( n in dom (Line (B9,i)) & j = (width A) + n ) ; :: thesis: contradiction

then consider n being Nat such that

A73: n in dom (Line (B9,i)) and

A74: j = (width A) + n ;

A75: [i,n] in Indices B by A58, A69, A67, A73, ZFMISC_1:87;

A76: B = 0. (K,(len A),(width B)) by A53, A61, Th52;

(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by A59, A64, MATRIX_0:def 7

.= (Line (B9,i)) . n by A66, A70, A73, A74, FINSEQ_1:def 7

.= B9 * (i,n) by A67, A73, MATRIX_0:def 7

.= 0. K by A75, A76, MATRIX_3:1 ;

hence contradiction by A63; :: thesis: verum

end;A73: n in dom (Line (B9,i)) and

A74: j = (width A) + n ;

A75: [i,n] in Indices B by A58, A69, A67, A73, ZFMISC_1:87;

A76: B = 0. (K,(len A),(width B)) by A53, A61, Th52;

(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by A59, A64, MATRIX_0:def 7

.= (Line (B9,i)) . n by A66, A70, A73, A74, FINSEQ_1:def 7

.= B9 * (i,n) by A67, A73, MATRIX_0:def 7

.= 0. K by A75, A76, MATRIX_3:1 ;

hence contradiction by A63; :: thesis: verum