let K be Field; :: thesis:
let A, B be Matrix of K; :: thesis:
assume A1: ( the_rank_of A = the_rank_of (A ^^ B) & len A = len B ) ; :: thesis:
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;
reconsider B' = B as Matrix of len A, width B,K by A1, MATRIX_2:7;
set AB = A' ^^ B';
let N be finite without_zero Subset of NAT ; :: thesis:
assume that
A2: N c= dom A and
A3: for i being Nat st i in N holds
Line A,i = (width A) |-> (0. K) ; :: thesis:
let i be Nat; :: thesis:
assume A4: i in N ; :: thesis:
assume Line B,i <> (width B) |-> (0. K) ; :: thesis:
then consider j being Nat such that
A5: ( j in Seg (width B) & (Line B,i) . j <> ((width B) |-> (0. K)) . j ) by FINSEQ_2:139;
A6: dom A = Seg (len A) by FINSEQ_1:def 3;
len A <> 0 by A2, A4, FINSEQ_1:4, FINSEQ_1:def 3;
then len A > 0 ;
then A7: ( width (A' ^^ B') = (width A) + (width B) & dom (A' ^^ B') = Seg (len (A' ^^ B')) & len (A' ^^ B') = len A & Indices (A' ^^ B') = [:(Seg (len A)),(Seg ((width A) + (width B))):] ) by FINSEQ_1:def 3, MATRIX_1:24;
then A8: j + (width A) in Seg (width (A' ^^ B')) by A5, FINSEQ_1:81;
A9: ( len (Line B',i) = width B' & len (Line A',i) = width A' ) by MATRIX_1:def 8;
then A10: ( 1 <= j & j <= len (Line B',i) ) by A5, FINSEQ_1:3;
(A' ^^ B') * i,(j + (width A)) = (Line (A' ^^ B'),i) . (j + (width A)) by A8, MATRIX_1:def 8
.= ((Line A',i) ^ (Line B',i)) . (j + (width A)) by A2, A4, A6, Th15
.= (Line B',i) . j by A9, A10, FINSEQ_1:86 ;
then A11: (A' ^^ B') * i,(j + (width A)) <> 0. K by A5, FINSEQ_2:71;
consider P, Q being finite without_zero Subset of NAT such that
A12: ( [:P,Q:] c= Indices A' & card P = card Q ) and
A13: card P = the_rank_of A' and
A14: Det (EqSegm A',P,Q) <> 0. K by MATRIX13:def 4;
A15: Segm (A' ^^ B'),(Seg (len A)),(Seg (width A)) = A by Th19;
( P = {} iff Q = {} ) by A12;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A16: ( P2 c= Seg (len A) & Q2 c= Seg (width A) ) and
A17: ( P2 = (Sgm (Seg (len A))) .: P & Q2 = (Sgm (Seg (width A))) .: Q ) and
( card P2 = card P & card Q2 = card Q ) and
A18: Segm A,P,Q = Segm (A' ^^ B'),P2,Q2 by A12, A15, MATRIX13:57;
width A <= width (A' ^^ B') by A7, NAT_1:11;
then A19: Seg (width A) c= Seg (width (A' ^^ B')) by FINSEQ_1:7;
then A20: [:P2,(Seg (width A)):] c= Indices (A' ^^ B') by A16, A7, ZFMISC_1:119;
not i in P2

proof

assume A21: i in P2 ; :: thesis:
A22: Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:54
.= id (Seg (len A)) ;
A23: ( P c= Seg (len A) & Q c= Seg (width A) ) by A12, MATRIX13:67;
then A24: i in P by A21, A17, A22, FUNCT_1:162;
A25: ( dom (Sgm P) = Seg (card P) & rng (Sgm P) = P & dom (Sgm Q) = Seg (card Q) & rng (Sgm Q) = Q ) by A23, FINSEQ_1:def 13, FINSEQ_3:45;
then consider x being set such that
A26: ( x in dom (Sgm P) & (Sgm P) . x = i ) by A24, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A26;
A27: dom (Line A,i) = Seg (width A) by FINSEQ_2:144;
Line A,i = (width A) |-> (0. K) by A3, A4
.= (0. K) * (Line A,i) by FVSUM_1:71 ;
then ( Line (Segm A,P,Q),x = ((0. K) * (Line A,i)) * (Sgm Q) & Line (Segm A,P,Q),x = (Line A,i) * (Sgm Q) ) by A23, A25, A26, MATRIX13:47;
then ( Line (Segm A,P,Q),x = (0. K) * (Line (Segm A,P,Q),x) & Segm A,P,Q = EqSegm A,P,Q ) by A12, A23, A25, A27, MATRIX13:87, MATRIX13:def 3;
then (0. K) * (Det (EqSegm A,P,Q)) = Det (RLine (EqSegm A,P,Q),x,(Line (EqSegm A,P,Q),x)) by A25, A26, MATRIX11:35
.= Det (EqSegm A,P,Q) by MATRIX11:30 ;
hence contradiction by A14, VECTSP_1:36; :: thesis:

end;

then A28: i in (dom (A' ^^ B')) \ P2 by A2, A4, A6, A7, XBOOLE_0:def 5;
j >= 1 by A5, FINSEQ_1:3;
then j + (width A) >= 1 + (width A) by XREAL_1:8;
then j + (width A) > width A by NAT_1:13;
then not j + (width A) in Q2 by A16, FINSEQ_1:3;
then A29: j + (width A) in (Seg (width (A' ^^ B'))) \ Q2 by A8, XBOOLE_0:def 5;
A30: ( card (Seg (len A)) = len A & card (Seg (width A)) = width A ) by FINSEQ_1:78;
A31: (Sgm (Seg (len A))) . i = (idseq (len A)) . i by FINSEQ_3:54
.= i by A6, A2, A4, FINSEQ_2:57 ;
(card (Seg (width A))) |-> (0. K) = Line A,i by A3, A4, A30
.= (Line (A' ^^ B'),i) * (Sgm (Seg (width A))) by A31, A30, A19, A15, A2, A4, A6, MATRIX13:47 ;
then A32: card P > the_rank_of (Segm (A' ^^ B'),P2,Q2) by A1, A16, Th10, A20, A28, A29, A11, A13;
Segm (A' ^^ B'),P2,Q2 = EqSegm A,P,Q by A12, A18, MATRIX13:def 3;
hence contradiction by A32, A14, MATRIX13:83; :: thesis: