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 ())) = A & Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))) = 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 ())) = A & Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))) = 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 ())) = A & Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))) = B )

let B be Matrix of n,k,D; :: thesis: ( Segm ((A ^^ B),(Seg n),(Seg ())) = A & Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))) = 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 ()));
A3: card (Seg ()) = 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 ()))) * (i,j) = A * (i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices A9 implies (Segm ((A ^^ B),(Seg n),(Seg ()))) * (i,j) = A * (i,j) )
assume A5: [i,j] in Indices A9 ; :: thesis: (Segm ((A ^^ B),(Seg n),(Seg ()))) * (i,j) = A * (i,j)
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
A6: dom A = Seg n by ;
n <> 0 by ;
then Indices A9 = [:(Seg n),(Seg ()):] by MATRIX_0:23;
then A7: I in Seg n by ;
A8: J in Seg () by ;
then A9: J = (idseq ()) . J by FINSEQ_2:49
.= (Sgm (Seg ())) . J by FINSEQ_3:48 ;
dom (Segm ((A ^^ B),(Seg n),(Seg ()))) = Seg (len (Segm ((A ^^ B),(Seg n),(Seg ())))) by FINSEQ_1:def 3
.= Seg n by ;
hence (Segm ((A ^^ B),(Seg n),(Seg ()))) * (i,j) = (Col ((Segm ((A ^^ B),(Seg n),(Seg ()))),J)) . I by
.= (Col ((A ^^ B),((Sgm (Seg ())) . J))) . I by
.= (Col (A,J)) . I by A8, A9, Th16
.= A * (i,j) by ;
:: thesis: verum
end;
hence A = Segm ((A ^^ B),(Seg n),(Seg ())) by ; :: thesis: Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))) = B
set w = () + ();
set SS = (Seg (() + ())) \ (Seg ());
set S2 = Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())));
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 <= () + () by NAT_1:11;
then ( card (Seg (() + ())) = () + () & Seg () c= Seg (() + ()) ) by ;
then A11: card ((Seg (() + ())) \ (Seg ())) = (() + ()) - () by
.= width B ;
now :: thesis: for i, j being Nat st [i,j] in Indices B9 holds
(Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())))) * (i,j) = B9 * (i,j)
A12: dom B = Seg n by ;
let i, j be Nat; :: thesis: ( [i,j] in Indices B9 implies (Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())))) * (i,j) = B9 * (i,j) )
assume A13: [i,j] in Indices B9 ; :: thesis: (Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())))) * (i,j) = B9 * (i,j)
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
A14: J in Seg () by ;
n <> 0 by ;
then Indices B9 = [:(Seg n),(Seg ()):] by MATRIX_0:23;
then A15: I in Seg n by ;
dom (Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())))) = Seg (len (Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))))) by FINSEQ_1:def 3
.= Seg n by ;
hence (Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())))) * (i,j) = (Col ((Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ())))),J)) . I by
.= (Col ((A ^^ B),((Sgm ((Seg (() + ())) \ (Seg ()))) . J))) . I by
.= (Col ((A ^^ B),(() + J))) . I by
.= (Col (B,J)) . I by
.= B9 * (i,j) by ;
:: thesis: verum
end;
hence Segm ((A ^^ B),(Seg n),((Seg (() + ())) \ (Seg ()))) = B by ; :: thesis: verum