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;

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 ;

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)

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(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;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

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)

hence
Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B
by A1, A11, MATRIX_0:27; :: thesis: verum(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;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