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) = () |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = () |-> (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) = () |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = () |-> (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) = () |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = () |-> (0. K)

reconsider B9 = B as Matrix of len A, width B,K by ;
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) = () |-> (0. K) ) implies for i being Nat st i in N holds
Line (B,i) = () |-> (0. K) )

assume that
A3: N c= dom A and
A4: for i being Nat st i in N holds
Line (A,i) = () |-> (0. K) ; :: thesis: for i being Nat st i in N holds
Line (B,i) = () |-> (0. K)

let i be Nat; :: thesis: ( i in N implies Line (B,i) = () |-> (0. K) )
assume A5: i in N ; :: thesis: Line (B,i) = () |-> (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) = () + () by MATRIX_0:23;
then width A <= width (A9 ^^ B9) by NAT_1:11;
then A8: Seg () 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 ())) = 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 ;
card (Seg ()) = width A by FINSEQ_1:57;
then A13: (card (Seg ())) |-> (0. K) = Line (A,i) by A4, A5
.= (Line ((A9 ^^ B9),i)) * (Sgm (Seg ())) by A3, A5, A11, A10, A8, A9, A12, MATRIX13:47 ;
assume Line (B,i) <> () |-> (0. K) ; :: thesis: contradiction
then consider j being Nat such that
A14: j in Seg () and
A15: (Line (B,i)) . j <> (() |-> (0. K)) . j by FINSEQ_2:119;
A16: ( len (Line (A9,i)) = width A9 & 1 <= j ) by ;
len (Line (B9,i)) = width B9 by MATRIX_0:def 7;
then A17: j <= len (Line (B9,i)) by ;
A18: j + () in Seg (width (A9 ^^ B9)) by ;
then (A9 ^^ B9) * (i,(j + ())) = (Line ((A9 ^^ B9),i)) . (j + ()) by MATRIX_0:def 7
.= ((Line (A9,i)) ^ (Line (B9,i))) . (j + ()) by A3, A5, A11, Th15
.= (Line (B9,i)) . j by ;
then A19: (A9 ^^ B9) * (i,(j + ())) <> 0. K by ;
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 () and
A26: P2 = (Sgm (Seg (len A))) .: P and
Q2 = (Sgm (Seg ())) .: Q and
card P2 = card P and
card Q2 = card Q and
A27: Segm (A,P,Q) = Segm ((A9 ^^ B9),P2,Q2) by ;
A28: Segm ((A9 ^^ B9),P2,Q2) = EqSegm (A,P,Q) by ;
A29: ( dom (A9 ^^ B9) = Seg (len (A9 ^^ B9)) & len (A9 ^^ B9) = len A ) by ;
then A30: [:P2,(Seg ()):] c= Indices (A9 ^^ B9) by ;
j >= 1 by ;
then j + () >= 1 + () by XREAL_1:6;
then j + () > width A by NAT_1:13;
then not j + () in Q2 by ;
then A31: j + () in (Seg (width (A9 ^^ B9))) \ Q2 by ;
not i in P2
proof
A32: Line (A,i) = () |-> (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 ;
then A35: rng (Sgm P) = P by FINSEQ_1:def 13;
assume i in P2 ; :: thesis: contradiction
then i in P by ;
then consider x being object such that
A36: x in dom (Sgm P) and
A37: (Sgm P) . x = i by ;
reconsider x = x as Element of NAT by A36;
A38: Segm (A,P,Q) = EqSegm (A,P,Q) by ;
A39: Q c= Seg () by ;
then A40: rng (Sgm Q) = Q by FINSEQ_1:def 13;
A41: dom (Sgm P) = Seg (card P) by ;
then ( dom (Line (A,i)) = Seg () & Line ((Segm (A,P,Q)),x) = (Line (A,i)) * (Sgm Q) ) by ;
then Line ((Segm (A,P,Q)),x) = (0. K) * (Line ((Segm (A,P,Q)),x)) by ;
then (0. K) * (Det (EqSegm (A,P,Q))) = Det (RLine ((EqSegm (A,P,Q)),x,(Line ((EqSegm (A,P,Q)),x)))) by
.= Det (EqSegm (A,P,Q)) by MATRIX11:30 ;
hence contradiction by A23; :: thesis: verum
end;
then i in (dom (A9 ^^ B9)) \ P2 by ;
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