let k, m, n 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:57;
A2: len A = n by MATRIX_0:def 2;
then reconsider A9 = A as Matrix of n, width A,D by MATRIX_0:51;
set S1 = Segm ((A ^^ B),(Seg n),(Seg (width A)));
A3: card (Seg (width A)) = width A by FINSEQ_1:57;
A4: len (A ^^ B) = n by MATRIX_0:def 2;

now :: thesis: for i, j being Nat st [i,j] in Indices A9 holds
(Segm ((A ^^ B),(Seg n),(Seg (width A)))) * (i,j) = A * (i,j)

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 12;
A6: dom A = Seg n by A2, FINSEQ_1:def 3;
n <> 0 by A5, MATRIX_0:22;
then Indices A9 = [:(Seg n),(Seg (width A)):] by MATRIX_0:23;
then A7: I in Seg n by A5, ZFMISC_1:87;
A8: J in Seg (width A) by A5, ZFMISC_1:87;
then A9: J = (idseq (width A)) . J by FINSEQ_2:49
.= (Sgm (Seg (width A))) . J by FINSEQ_3:48 ;
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_0:def 2 ;
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_0:def 8
.= (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_0:def 8 ;
:: thesis: verum

end;

hence A = Segm ((A ^^ B),(Seg n),(Seg (width A))) by A1, A3, MATRIX_0:27; :: 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_0:def 2;
then reconsider B9 = B as Matrix of n, width B,D by MATRIX_0:51;
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:5, FINSEQ_1:57;
then A11: card ((Seg ((width A) + (width B))) \ (Seg (width A))) = ((width A) + (width B)) - (width A) by A3, CARD_2:44
.= width B ;

now :: thesis: for i, j being Nat st [i,j] in Indices B9 holds
(Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) * (i,j) = B9 * (i,j)

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 12;
A14: J in Seg (width B) by A13, ZFMISC_1:87;
n <> 0 by A13, MATRIX_0:22;
then Indices B9 = [:(Seg n),(Seg (width B)):] by MATRIX_0:23;
then A15: I in Seg n by A13, ZFMISC_1:87;
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_0:def 2 ;
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_0:def 8
.= (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_0:def 8 ;
:: thesis: verum

end;

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