let D be non empty set ; :: thesis:
let A be Matrix of D; :: thesis:
let Bx, By, Cx, Cy be finite without_zero Subset of NAT; :: thesis:
assume that
A1: [:Bx,By:] c= Indices A and
A2: [:Cx,Cy:] c= Indices A ; :: thesis:
set w = width A;
set l = len A;
set cy = card Cy;
set cx = card Cx;
set bY = card By;
set bx = card Bx;
let B be Matrix of card Bx, card By,D; :: thesis:
let C be Matrix of card Cx, card Cy,D; :: thesis:
assume A3: for i, j, bi, bj, ci, cj being Nat st [i,j] in [:Bx,By:] /\ [:Cx,Cy:] & bi = ((Sgm Bx) ") . i & bj = ((Sgm By) ") . j & ci = ((Sgm Cx) ") . i & cj = ((Sgm Cy) ") . j holds
B * (bi,bj) = C * (ci,cj) ; :: thesis:
A4: ex kBy being Nat st By c= Seg kBy by MATRIX13:43;
then A5: rng (Sgm By) = By by FINSEQ_1:def 13;
defpred S₁[ set , set , set ] means for i, j being Nat st $1 = i & $2 = j holds
( ( [i,j] in [:Bx,By:] implies ( ex m, n being Nat st
( m in dom (Sgm Bx) & n in dom (Sgm By) & (Sgm Bx) . m = i & (Sgm By) . n = j ) & ( for m, n being Nat st m in dom (Sgm Bx) & n in dom (Sgm By) & (Sgm Bx) . m = i & (Sgm By) . n = j holds
$3 = B * (m,n) ) ) ) & ( [i,j] in [:Cx,Cy:] implies ( ex m, n being Nat st
( m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j ) & ( for m, n being Nat st m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j holds
$3 = C * (m,n) ) ) ) & ( not [i,j] in [:Bx,By:] \/ [:Cx,Cy:] implies $3 = A * (i,j) ) );
A14: ex kBx being Nat st Bx c= Seg kBx by MATRIX13:43;
then A15: rng (Sgm Bx) = Bx by FINSEQ_1:def 13;
A16: dom (Sgm By) = Seg (card By) by A4, FINSEQ_3:40;
A17: Sgm By is one-to-one by A4, FINSEQ_3:92;
A18: Sgm Bx is one-to-one by A14, FINSEQ_3:92;
A19: ex kCy being Nat st Cy c= Seg kCy by MATRIX13:43;
then A20: rng (Sgm Cy) = Cy by FINSEQ_1:def 13;
A21: Sgm Cy is one-to-one by A19, FINSEQ_3:92;
A22: ex kCx being Nat st Cx c= Seg kCx by MATRIX13:43;
then A23: rng (Sgm Cx) = Cx by FINSEQ_1:def 13;
A24: Sgm Cx is one-to-one by A22, FINSEQ_3:92;
A25: for i, j being Nat st [i,j] in [:(Seg (len A)),(Seg (width A)):] holds
ex x being Element of D st S₁[i,j,x]

let i, j be Nat; :: thesis:
assume [i,j] in [:(Seg (len A)),(Seg (width A)):] ; :: thesis:

per cases in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) or ( [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] ) or ( not [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) or ( not [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] ) ) ;

suppose A26: ( [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) ; :: thesis:

then j in Cy by ZFMISC_1:87;
then consider yC being set such that
A27: yC in dom (Sgm Cy) and
A28: (Sgm Cy) . yC = j by A20, FUNCT_1:def 3;
j in By by A26, ZFMISC_1:87;
then consider y being set such that
A29: y in dom (Sgm By) and
A30: (Sgm By) . y = j by A5, FUNCT_1:def 3;
i in Cx by A26, ZFMISC_1:87;
then consider xC being set such that
A31: xC in dom (Sgm Cx) and
A32: (Sgm Cx) . xC = i by A23, FUNCT_1:def 3;
i in Bx by A26, ZFMISC_1:87;
then consider x being set such that
A33: x in dom (Sgm Bx) and
A34: (Sgm Bx) . x = i by A15, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A33, A29;
take BB = B * (x,y); :: thesis:

A35: now

let m, n be Nat; :: thesis:
assume ( m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j ) ; :: thesis:
then A36: ( ((Sgm Cx) ") . i = m & ((Sgm Cy) ") . j = n ) by A24, A21, FUNCT_1:32;
A37: ((Sgm By) ") . j = y by A17, A29, A30, FUNCT_1:32;
( [i,j] in [:Bx,By:] /\ [:Cx,Cy:] & ((Sgm Bx) ") . i = x ) by A18, A26, A33, A34, FUNCT_1:32, XBOOLE_0:def 4;
hence BB = C * (m,n) by A3, A37, A36; :: thesis:

end;

now

let m, n be Nat; :: thesis:
assume that
A38: m in dom (Sgm Bx) and
A39: n in dom (Sgm By) and
A40: (Sgm Bx) . m = i and
A41: (Sgm By) . n = j ; :: thesis:
x = m by A18, A33, A34, A38, A40, FUNCT_1:def 4;
hence BB = B * (m,n) by A17, A29, A30, A39, A41, FUNCT_1:def 4; :: thesis:

end;

hence S₁[i,j,BB] by A26, A33, A34, A29, A30, A31, A32, A27, A28, A35, XBOOLE_0:def 3; :: thesis:

end;

suppose A42: ( [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] ) ; :: thesis:

then j in By by ZFMISC_1:87;
then consider y being set such that
A43: y in dom (Sgm By) and
A44: (Sgm By) . y = j by A5, FUNCT_1:def 3;
i in Bx by A42, ZFMISC_1:87;
then consider x being set such that
A45: x in dom (Sgm Bx) and
A46: (Sgm Bx) . x = i by A15, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A45, A43;
take BB = B * (x,y); :: thesis:

now

let m, n be Nat; :: thesis:
assume that
A47: m in dom (Sgm Bx) and
A48: n in dom (Sgm By) and
A49: (Sgm Bx) . m = i and
A50: (Sgm By) . n = j ; :: thesis:
x = m by A18, A45, A46, A47, A49, FUNCT_1:def 4;
hence BB = B * (m,n) by A17, A43, A44, A48, A50, FUNCT_1:def 4; :: thesis:

end;

hence S₁[i,j,BB] by A42, A45, A46, A43, A44, XBOOLE_0:def 3; :: thesis:

end;

suppose A51: ( not [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) ; :: thesis:

then j in Cy by ZFMISC_1:87;
then consider y being set such that
A52: y in dom (Sgm Cy) and
A53: (Sgm Cy) . y = j by A20, FUNCT_1:def 3;
i in Cx by A51, ZFMISC_1:87;
then consider x being set such that
A54: x in dom (Sgm Cx) and
A55: (Sgm Cx) . x = i by A23, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A54, A52;
take CC = C * (x,y); :: thesis:

now

let m, n be Nat; :: thesis:
assume that
A56: m in dom (Sgm Cx) and
A57: n in dom (Sgm Cy) and
A58: (Sgm Cx) . m = i and
A59: (Sgm Cy) . n = j ; :: thesis:
x = m by A24, A54, A55, A56, A58, FUNCT_1:def 4;
hence CC = C * (m,n) by A21, A52, A53, A57, A59, FUNCT_1:def 4; :: thesis:

end;

hence S₁[i,j,CC] by A51, A54, A55, A52, A53, XBOOLE_0:def 3; :: thesis:

end;

suppose A60: ( not [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] ) ; :: thesis:

take A * (i,j) ; :: thesis:
thus S₁[i,j,A * (i,j)] by A60; :: thesis:

end;

consider M being Matrix of len A, width A,D such that
A61: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_1:sch 2(A25);
set MB = Segm (M,Bx,By);
take M ; :: thesis:
A is Matrix of len A, width A,D by MATRIX_2:7;
then A62: Indices A = Indices M by MATRIX_1:26;
A63: dom (Sgm Bx) = Seg (card Bx) by A14, FINSEQ_3:40;

now

let i, j be Nat; :: thesis:
assume A64: [i,j] in Indices (Segm (M,Bx,By)) ; :: thesis:
card Bx <> 0 by A64, MATRIX_1:22;
then A65: Indices (Segm (M,Bx,By)) = [:(Seg (card Bx)),(Seg (card By)):] by MATRIX_1:23;
then A66: j in Seg (card By) by A64, ZFMISC_1:87;
then A67: (Sgm By) . j in By by A5, A16, FUNCT_1:def 3;
A68: i in Seg (card Bx) by A64, A65, ZFMISC_1:87;
then (Sgm Bx) . i in Bx by A15, A63, FUNCT_1:def 3;
then [((Sgm Bx) . i),((Sgm By) . j)] in [:Bx,By:] by A67, ZFMISC_1:87;
hence B * (i,j) = M * (((Sgm Bx) . i),((Sgm By) . j)) by A1, A63, A16, A61, A62, A68, A66
.= (Segm (M,Bx,By)) * (i,j) by A64, MATRIX13:def 1 ;
:: thesis:

end;

hence Segm (M,Bx,By) = B by MATRIX_1:27; :: thesis:
set MC = Segm (M,Cx,Cy);
A69: dom (Sgm Cy) = Seg (card Cy) by A19, FINSEQ_3:40;
A70: dom (Sgm Cx) = Seg (card Cx) by A22, FINSEQ_3:40;

now

let i, j be Nat; :: thesis:
assume A71: [i,j] in Indices (Segm (M,Cx,Cy)) ; :: thesis:
card Cx <> 0 by A71, MATRIX_1:22;
then A72: Indices (Segm (M,Cx,Cy)) = [:(Seg (card Cx)),(Seg (card Cy)):] by MATRIX_1:23;
then A73: j in Seg (card Cy) by A71, ZFMISC_1:87;
then A74: (Sgm Cy) . j in Cy by A20, A69, FUNCT_1:def 3;
A75: i in Seg (card Cx) by A71, A72, ZFMISC_1:87;
then (Sgm Cx) . i in Cx by A23, A70, FUNCT_1:def 3;
then [((Sgm Cx) . i),((Sgm Cy) . j)] in [:Cx,Cy:] by A74, ZFMISC_1:87;
hence C * (i,j) = M * (((Sgm Cx) . i),((Sgm Cy) . j)) by A2, A70, A69, A61, A62, A75, A73
.= (Segm (M,Cx,Cy)) * (i,j) by A71, MATRIX13:def 1 ;
:: thesis:

end;

hence Segm (M,Cx,Cy) = C by MATRIX_1:27; :: thesis:
let i, j be Nat; :: thesis:
assume A76: [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) ; :: thesis:
not [i,j] in [:Bx,By:] \/ [:Cx,Cy:] by A76, XBOOLE_0:def 5;
hence M * (i,j) = A * (i,j) by A61, A76; :: thesis: