let K be Field; :: thesis: for A, B being Matrix of K st the_rank_of A = the_rank_of (A ^^ B) & len A = len B holds

for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds

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

for i being Nat st i in N holds

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

let A, B be Matrix of K; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) & len A = len B implies for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds

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

for i being Nat st i in N holds

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

assume that

A1: the_rank_of A = the_rank_of (A ^^ B) and

A2: len A = len B ; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds

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

for i being Nat st i in N holds

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

reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_0:51;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set AB = A9 ^^ B9;

let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & ( for i being Nat st i in N holds

Line (A,i) = (width A) |-> (0. K) ) implies for i being Nat st i in N holds

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

assume that

A3: N c= dom A and

A4: for i being Nat st i in N holds

Line (A,i) = (width A) |-> (0. K) ; :: thesis: for i being Nat st i in N holds

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

let i be Nat; :: thesis: ( i in N implies Line (B,i) = (width B) |-> (0. K) )

assume A5: i in N ; :: thesis: Line (B,i) = (width B) |-> (0. K)

dom A <> {} by A3, A5;

then Seg (len A) <> {} by FINSEQ_1:def 3;

then A6: len A <> 0 ;

then A7: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_0:23;

then width A <= width (A9 ^^ B9) by NAT_1:11;

then A8: Seg (width A) c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;

A9: card (Seg (len A)) = len A by FINSEQ_1:57;

A10: Segm ((A9 ^^ B9),(Seg (len A)),(Seg (width A))) = A by Th19;

A11: dom A = Seg (len A) by FINSEQ_1:def 3;

A12: (Sgm (Seg (len A))) . i = (idseq (len A)) . i by FINSEQ_3:48

.= i by A3, A5, A11, FINSEQ_2:49 ;

card (Seg (width A)) = width A by FINSEQ_1:57;

then A13: (card (Seg (width A))) |-> (0. K) = Line (A,i) by A4, A5

.= (Line ((A9 ^^ B9),i)) * (Sgm (Seg (width A))) by A3, A5, A11, A10, A8, A9, A12, MATRIX13:47 ;

assume Line (B,i) <> (width B) |-> (0. K) ; :: thesis: contradiction

then consider j being Nat such that

A14: j in Seg (width B) and

A15: (Line (B,i)) . j <> ((width B) |-> (0. K)) . j by FINSEQ_2:119;

A16: ( len (Line (A9,i)) = width A9 & 1 <= j ) by A14, FINSEQ_1:1, MATRIX_0:def 7;

len (Line (B9,i)) = width B9 by MATRIX_0:def 7;

then A17: j <= len (Line (B9,i)) by A14, FINSEQ_1:1;

A18: j + (width A) in Seg (width (A9 ^^ B9)) by A14, A7, FINSEQ_1:60;

then (A9 ^^ B9) * (i,(j + (width A))) = (Line ((A9 ^^ B9),i)) . (j + (width A)) by MATRIX_0:def 7

.= ((Line (A9,i)) ^ (Line (B9,i))) . (j + (width A)) by A3, A5, A11, Th15

.= (Line (B9,i)) . j by A16, A17, FINSEQ_1:65 ;

then A19: (A9 ^^ B9) * (i,(j + (width A))) <> 0. K by A14, A15, FINSEQ_2:57;

consider P, Q being finite without_zero Subset of NAT such that

A20: [:P,Q:] c= Indices A9 and

A21: card P = card Q and

A22: card P = the_rank_of A9 and

A23: Det (EqSegm (A9,P,Q)) <> 0. K by MATRIX13:def 4;

( P = {} iff Q = {} ) by A21;

then consider P2, Q2 being finite without_zero Subset of NAT such that

A24: P2 c= Seg (len A) and

A25: Q2 c= Seg (width A) and

A26: P2 = (Sgm (Seg (len A))) .: P and

Q2 = (Sgm (Seg (width A))) .: Q and

card P2 = card P and

card Q2 = card Q and

A27: Segm (A,P,Q) = Segm ((A9 ^^ B9),P2,Q2) by A20, A10, MATRIX13:57;

A28: Segm ((A9 ^^ B9),P2,Q2) = EqSegm (A,P,Q) by A21, A27, MATRIX13:def 3;

A29: ( dom (A9 ^^ B9) = Seg (len (A9 ^^ B9)) & len (A9 ^^ B9) = len A ) by A6, FINSEQ_1:def 3, MATRIX_0:23;

then A30: [:P2,(Seg (width A)):] c= Indices (A9 ^^ B9) by A24, A8, ZFMISC_1:96;

j >= 1 by A14, FINSEQ_1:1;

then j + (width A) >= 1 + (width A) by XREAL_1:6;

then j + (width A) > width A by NAT_1:13;

then not j + (width A) in Q2 by A25, FINSEQ_1:1;

then A31: j + (width A) in (Seg (width (A9 ^^ B9))) \ Q2 by A18, XBOOLE_0:def 5;

not i in P2

then card P > the_rank_of (Segm ((A9 ^^ B9),P2,Q2)) by A1, A19, A22, A25, A30, A31, A13, Th10;

hence contradiction by A23, A28, MATRIX13:83; :: thesis: verum

for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds

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

for i being Nat st i in N holds

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

let A, B be Matrix of K; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) & len A = len B implies for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds

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

for i being Nat st i in N holds

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

assume that

A1: the_rank_of A = the_rank_of (A ^^ B) and

A2: len A = len B ; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds

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

for i being Nat st i in N holds

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

reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_0:51;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set AB = A9 ^^ B9;

let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & ( for i being Nat st i in N holds

Line (A,i) = (width A) |-> (0. K) ) implies for i being Nat st i in N holds

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

assume that

A3: N c= dom A and

A4: for i being Nat st i in N holds

Line (A,i) = (width A) |-> (0. K) ; :: thesis: for i being Nat st i in N holds

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

let i be Nat; :: thesis: ( i in N implies Line (B,i) = (width B) |-> (0. K) )

assume A5: i in N ; :: thesis: Line (B,i) = (width B) |-> (0. K)

dom A <> {} by A3, A5;

then Seg (len A) <> {} by FINSEQ_1:def 3;

then A6: len A <> 0 ;

then A7: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_0:23;

then width A <= width (A9 ^^ B9) by NAT_1:11;

then A8: Seg (width A) c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;

A9: card (Seg (len A)) = len A by FINSEQ_1:57;

A10: Segm ((A9 ^^ B9),(Seg (len A)),(Seg (width A))) = A by Th19;

A11: dom A = Seg (len A) by FINSEQ_1:def 3;

A12: (Sgm (Seg (len A))) . i = (idseq (len A)) . i by FINSEQ_3:48

.= i by A3, A5, A11, FINSEQ_2:49 ;

card (Seg (width A)) = width A by FINSEQ_1:57;

then A13: (card (Seg (width A))) |-> (0. K) = Line (A,i) by A4, A5

.= (Line ((A9 ^^ B9),i)) * (Sgm (Seg (width A))) by A3, A5, A11, A10, A8, A9, A12, MATRIX13:47 ;

assume Line (B,i) <> (width B) |-> (0. K) ; :: thesis: contradiction

then consider j being Nat such that

A14: j in Seg (width B) and

A15: (Line (B,i)) . j <> ((width B) |-> (0. K)) . j by FINSEQ_2:119;

A16: ( len (Line (A9,i)) = width A9 & 1 <= j ) by A14, FINSEQ_1:1, MATRIX_0:def 7;

len (Line (B9,i)) = width B9 by MATRIX_0:def 7;

then A17: j <= len (Line (B9,i)) by A14, FINSEQ_1:1;

A18: j + (width A) in Seg (width (A9 ^^ B9)) by A14, A7, FINSEQ_1:60;

then (A9 ^^ B9) * (i,(j + (width A))) = (Line ((A9 ^^ B9),i)) . (j + (width A)) by MATRIX_0:def 7

.= ((Line (A9,i)) ^ (Line (B9,i))) . (j + (width A)) by A3, A5, A11, Th15

.= (Line (B9,i)) . j by A16, A17, FINSEQ_1:65 ;

then A19: (A9 ^^ B9) * (i,(j + (width A))) <> 0. K by A14, A15, FINSEQ_2:57;

consider P, Q being finite without_zero Subset of NAT such that

A20: [:P,Q:] c= Indices A9 and

A21: card P = card Q and

A22: card P = the_rank_of A9 and

A23: Det (EqSegm (A9,P,Q)) <> 0. K by MATRIX13:def 4;

( P = {} iff Q = {} ) by A21;

then consider P2, Q2 being finite without_zero Subset of NAT such that

A24: P2 c= Seg (len A) and

A25: Q2 c= Seg (width A) and

A26: P2 = (Sgm (Seg (len A))) .: P and

Q2 = (Sgm (Seg (width A))) .: Q and

card P2 = card P and

card Q2 = card Q and

A27: Segm (A,P,Q) = Segm ((A9 ^^ B9),P2,Q2) by A20, A10, MATRIX13:57;

A28: Segm ((A9 ^^ B9),P2,Q2) = EqSegm (A,P,Q) by A21, A27, MATRIX13:def 3;

A29: ( dom (A9 ^^ B9) = Seg (len (A9 ^^ B9)) & len (A9 ^^ B9) = len A ) by A6, FINSEQ_1:def 3, MATRIX_0:23;

then A30: [:P2,(Seg (width A)):] c= Indices (A9 ^^ B9) by A24, A8, ZFMISC_1:96;

j >= 1 by A14, FINSEQ_1:1;

then j + (width A) >= 1 + (width A) by XREAL_1:6;

then j + (width A) > width A by NAT_1:13;

then not j + (width A) in Q2 by A25, FINSEQ_1:1;

then A31: j + (width A) in (Seg (width (A9 ^^ B9))) \ Q2 by A18, XBOOLE_0:def 5;

not i in P2

proof

then
i in (dom (A9 ^^ B9)) \ P2
by A3, A5, A11, A29, XBOOLE_0:def 5;
A32: Line (A,i) =
(width A) |-> (0. K)
by A4, A5

.= (0. K) * (Line (A,i)) by FVSUM_1:58 ;

A33: Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:48

.= id (Seg (len A)) ;

A34: P c= Seg (len A) by A20, A21, MATRIX13:67;

then A35: rng (Sgm P) = P by FINSEQ_1:def 13;

assume i in P2 ; :: thesis: contradiction

then i in P by A26, A33, A34, FUNCT_1:92;

then consider x being object such that

A36: x in dom (Sgm P) and

A37: (Sgm P) . x = i by A35, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A36;

A38: Segm (A,P,Q) = EqSegm (A,P,Q) by A21, MATRIX13:def 3;

A39: Q c= Seg (width A) by A20, A21, MATRIX13:67;

then A40: rng (Sgm Q) = Q by FINSEQ_1:def 13;

A41: dom (Sgm P) = Seg (card P) by A34, FINSEQ_3:40;

then ( dom (Line (A,i)) = Seg (width A) & Line ((Segm (A,P,Q)),x) = (Line (A,i)) * (Sgm Q) ) by A39, A36, A37, FINSEQ_2:124, MATRIX13:47;

then Line ((Segm (A,P,Q)),x) = (0. K) * (Line ((Segm (A,P,Q)),x)) by A39, A40, A32, MATRIX13:87;

then (0. K) * (Det (EqSegm (A,P,Q))) = Det (RLine ((EqSegm (A,P,Q)),x,(Line ((EqSegm (A,P,Q)),x)))) by A41, A36, A38, MATRIX11:35

.= Det (EqSegm (A,P,Q)) by MATRIX11:30 ;

hence contradiction by A23; :: thesis: verum

end;.= (0. K) * (Line (A,i)) by FVSUM_1:58 ;

A33: Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:48

.= id (Seg (len A)) ;

A34: P c= Seg (len A) by A20, A21, MATRIX13:67;

then A35: rng (Sgm P) = P by FINSEQ_1:def 13;

assume i in P2 ; :: thesis: contradiction

then i in P by A26, A33, A34, FUNCT_1:92;

then consider x being object such that

A36: x in dom (Sgm P) and

A37: (Sgm P) . x = i by A35, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A36;

A38: Segm (A,P,Q) = EqSegm (A,P,Q) by A21, MATRIX13:def 3;

A39: Q c= Seg (width A) by A20, A21, MATRIX13:67;

then A40: rng (Sgm Q) = Q by FINSEQ_1:def 13;

A41: dom (Sgm P) = Seg (card P) by A34, FINSEQ_3:40;

then ( dom (Line (A,i)) = Seg (width A) & Line ((Segm (A,P,Q)),x) = (Line (A,i)) * (Sgm Q) ) by A39, A36, A37, FINSEQ_2:124, MATRIX13:47;

then Line ((Segm (A,P,Q)),x) = (0. K) * (Line ((Segm (A,P,Q)),x)) by A39, A40, A32, MATRIX13:87;

then (0. K) * (Det (EqSegm (A,P,Q))) = Det (RLine ((EqSegm (A,P,Q)),x,(Line ((EqSegm (A,P,Q)),x)))) by A41, A36, A38, MATRIX11:35

.= Det (EqSegm (A,P,Q)) by MATRIX11:30 ;

hence contradiction by A23; :: thesis: verum

then card P > the_rank_of (Segm ((A9 ^^ B9),P2,Q2)) by A1, A19, A22, A25, A30, A31, A13, Th10;

hence contradiction by A23, A28, MATRIX13:83; :: thesis: verum