let n, m, k be Nat; :: thesis: for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D holds
( Segm (A ^^ B),(Seg n),(Seg (width A)) = A & Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B )
let D be non empty set ; :: thesis: for A being Matrix of n,m,D
for B being Matrix of n,k,D holds
( Segm (A ^^ B),(Seg n),(Seg (width A)) = A & Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B )
let A be Matrix of n,m,D; :: thesis: for B being Matrix of n,k,D holds
( Segm (A ^^ B),(Seg n),(Seg (width A)) = A & Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B )
let B be Matrix of n,k,D; :: thesis: ( Segm (A ^^ B),(Seg n),(Seg (width A)) = A & Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B )
set AB = A ^^ B;
A1: card (Seg n) = n by FINSEQ_1:78;
A2: len A = n by MATRIX_1:def 3;
then reconsider A9 = A as Matrix of n, width A,D by MATRIX_2:7;
set S1 = Segm (A ^^ B),(Seg n),(Seg (width A));
A3: card (Seg (width A)) = width A by FINSEQ_1:78;
A4: len (A ^^ B) = n by MATRIX_1:def 3;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices A9 implies (Segm (A ^^ B),(Seg n),(Seg (width A))) * i,j = A * i,j )
assume A5: [i,j] in Indices A9 ; :: thesis: (Segm (A ^^ B),(Seg n),(Seg (width A))) * i,j = A * i,j
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
A6: dom A = Seg n by A2, FINSEQ_1:def 3;
n <> 0 by A5, MATRIX_1:23;
then Indices A9 = [:(Seg n),(Seg (width A)):] by MATRIX_1:24;
then A7: I in Seg n by A5, ZFMISC_1:106;
A8: J in Seg (width A) by A5, ZFMISC_1:106;
then A9: J = (idseq (width A)) . J by FINSEQ_2:57
.= (Sgm (Seg (width A))) . J by FINSEQ_3:54 ;
dom (Segm (A ^^ B),(Seg n),(Seg (width A))) = Seg (len (Segm (A ^^ B),(Seg n),(Seg (width A)))) by FINSEQ_1:def 3
.= Seg n by A1, MATRIX_1:def 3 ;
hence (Segm (A ^^ B),(Seg n),(Seg (width A))) * i,j = (Col (Segm (A ^^ B),(Seg n),(Seg (width A))),J) . I by A7, MATRIX_1:def 9
.= (Col (A ^^ B),((Sgm (Seg (width A))) . J)) . I by A4, A3, A8, MATRIX13:50
.= (Col A,J) . I by A8, A9, Th16
.= A * i,j by A7, A6, MATRIX_1:def 9 ;
:: thesis: verum

end;

hence A = Segm (A ^^ B),(Seg n),(Seg (width A)) by A1, A3, MATRIX_1:28; :: thesis: Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B
set w = (width A) + (width B);
set SS = (Seg ((width A) + (width B))) \ (Seg (width A));
set S2 = Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)));
A10: len B = n by MATRIX_1:def 3;
then reconsider B9 = B as Matrix of n, width B,D by MATRIX_2:7;
width A <= (width A) + (width B) by NAT_1:11;
then ( card (Seg ((width A) + (width B))) = (width A) + (width B) & Seg (width A) c= Seg ((width A) + (width B)) ) by FINSEQ_1:7, FINSEQ_1:78;
then A11: card ((Seg ((width A) + (width B))) \ (Seg (width A))) = ((width A) + (width B)) - (width A) by A3, CARD_2:63
.= width B ;

now

A12: dom B = Seg n by A10, FINSEQ_1:def 3;
let i, j be Nat; :: thesis: ( [i,j] in Indices B9 implies (Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) * i,j = B9 * i,j )
assume A13: [i,j] in Indices B9 ; :: thesis: (Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) * i,j = B9 * i,j
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
A14: J in Seg (width B) by A13, ZFMISC_1:106;
n <> 0 by A13, MATRIX_1:23;
then Indices B9 = [:(Seg n),(Seg (width B)):] by MATRIX_1:24;
then A15: I in Seg n by A13, ZFMISC_1:106;
dom (Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = Seg (len (Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) by FINSEQ_1:def 3
.= Seg n by A1, MATRIX_1:def 3 ;
hence (Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) * i,j = (Col (Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))),J) . I by A15, MATRIX_1:def 9
.= (Col (A ^^ B),((Sgm ((Seg ((width A) + (width B))) \ (Seg (width A)))) . J)) . I by A4, A11, A14, MATRIX13:50
.= (Col (A ^^ B),((width A) + J)) . I by A14, Th8
.= (Col B,J) . I by A14, Th17
.= B9 * i,j by A15, A12, MATRIX_1:def 9 ;
:: thesis: verum

end;

hence Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B by A1, A11, MATRIX_1:28; :: thesis: verum