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) ) );
A6: ex kBx being Nat st Bx c= Seg kBx by MATRIX13:43;
then A7: rng (Sgm Bx) = Bx by FINSEQ_1:def 13;
A8: dom (Sgm By) = Seg (card By) by A4, FINSEQ_3:40;
A9: Sgm By is one-to-one by A4, FINSEQ_3:92;
A10: Sgm Bx is one-to-one by A6, FINSEQ_3:92;
A11: ex kCy being Nat st Cy c= Seg kCy by MATRIX13:43;
then A12: rng (Sgm Cy) = Cy by FINSEQ_1:def 13;
A13: Sgm Cy is one-to-one by A11, FINSEQ_3:92;
A14: ex kCx being Nat st Cx c= Seg kCx by MATRIX13:43;
then A15: rng (Sgm Cx) = Cx by FINSEQ_1:def 13;
A16: Sgm Cx is one-to-one by A14, FINSEQ_3:92;
A17: 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 A18: ( [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) ; :: thesis:

then j in Cy by ZFMISC_1:87;
then consider yC being object such that
A19: yC in dom (Sgm Cy) and
A20: (Sgm Cy) . yC = j by A12, FUNCT_1:def 3;
j in By by A18, ZFMISC_1:87;
then consider y being object such that
A21: y in dom (Sgm By) and
A22: (Sgm By) . y = j by A5, FUNCT_1:def 3;
i in Cx by A18, ZFMISC_1:87;
then consider xC being object such that
A23: xC in dom (Sgm Cx) and
A24: (Sgm Cx) . xC = i by A15, FUNCT_1:def 3;
i in Bx by A18, ZFMISC_1:87;
then consider x being object such that
A25: x in dom (Sgm Bx) and
A26: (Sgm Bx) . x = i by A7, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A25, A21;
take BB = B * (x,y); :: thesis:

A27: now :: thesis:

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 A28: ( ((Sgm Cx) ") . i = m & ((Sgm Cy) ") . j = n ) by A16, A13, FUNCT_1:32;
A29: ((Sgm By) ") . j = y by A9, A21, A22, FUNCT_1:32;
( [i,j] in [:Bx,By:] /\ [:Cx,Cy:] & ((Sgm Bx) ") . i = x ) by A10, A18, A25, A26, FUNCT_1:32, XBOOLE_0:def 4;
hence BB = C * (m,n) by A3, A29, A28; :: thesis:

end;

now :: thesis:

let m, n be Nat; :: thesis:
assume that
A30: m in dom (Sgm Bx) and
A31: n in dom (Sgm By) and
A32: (Sgm Bx) . m = i and
A33: (Sgm By) . n = j ; :: thesis:
x = m by A10, A25, A26, A30, A32, FUNCT_1:def 4;
hence BB = B * (m,n) by A9, A21, A22, A31, A33, FUNCT_1:def 4; :: thesis:

end;

hence S₁[i,j,BB] by A18, A25, A26, A21, A22, A23, A24, A19, A20, A27, XBOOLE_0:def 3; :: thesis:

end;

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

then j in By by ZFMISC_1:87;
then consider y being object such that
A35: y in dom (Sgm By) and
A36: (Sgm By) . y = j by A5, FUNCT_1:def 3;
i in Bx by A34, ZFMISC_1:87;
then consider x being object such that
A37: x in dom (Sgm Bx) and
A38: (Sgm Bx) . x = i by A7, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A37, A35;
take BB = B * (x,y); :: thesis:

now :: thesis:

let m, n be Nat; :: thesis:
assume that
A39: m in dom (Sgm Bx) and
A40: n in dom (Sgm By) and
A41: (Sgm Bx) . m = i and
A42: (Sgm By) . n = j ; :: thesis:
x = m by A10, A37, A38, A39, A41, FUNCT_1:def 4;
hence BB = B * (m,n) by A9, A35, A36, A40, A42, FUNCT_1:def 4; :: thesis:

end;

hence S₁[i,j,BB] by A34, A37, A38, A35, A36, XBOOLE_0:def 3; :: thesis:

end;

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

then j in Cy by ZFMISC_1:87;
then consider y being object such that
A44: y in dom (Sgm Cy) and
A45: (Sgm Cy) . y = j by A12, FUNCT_1:def 3;
i in Cx by A43, ZFMISC_1:87;
then consider x being object such that
A46: x in dom (Sgm Cx) and
A47: (Sgm Cx) . x = i by A15, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A46, A44;
take CC = C * (x,y); :: thesis:

now :: thesis:

let m, n be Nat; :: thesis:
assume that
A48: m in dom (Sgm Cx) and
A49: n in dom (Sgm Cy) and
A50: (Sgm Cx) . m = i and
A51: (Sgm Cy) . n = j ; :: thesis:
x = m by A16, A46, A47, A48, A50, FUNCT_1:def 4;
hence CC = C * (m,n) by A13, A44, A45, A49, A51, FUNCT_1:def 4; :: thesis:

end;

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

end;

suppose A52: ( 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 A52; :: thesis:

end;

consider M being Matrix of len A, width A,D such that
A53: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A17);
set MB = Segm (M,Bx,By);
take M ; :: thesis:
A is Matrix of len A, width A,D by MATRIX_0:51;
then A54: Indices A = Indices M by MATRIX_0:26;
A55: dom (Sgm Bx) = Seg (card Bx) by A6, FINSEQ_3:40;

now :: thesis:

let i, j be Nat; :: thesis:
assume A56: [i,j] in Indices (Segm (M,Bx,By)) ; :: thesis:
card Bx <> 0 by A56, MATRIX_0:22;
then A57: Indices (Segm (M,Bx,By)) = [:(Seg (card Bx)),(Seg (card By)):] by MATRIX_0:23;
then A58: j in Seg (card By) by A56, ZFMISC_1:87;
then A59: (Sgm By) . j in By by A5, A8, FUNCT_1:def 3;
A60: i in Seg (card Bx) by A56, A57, ZFMISC_1:87;
then (Sgm Bx) . i in Bx by A7, A55, FUNCT_1:def 3;
then [((Sgm Bx) . i),((Sgm By) . j)] in [:Bx,By:] by A59, ZFMISC_1:87;
hence B * (i,j) = M * (((Sgm Bx) . i),((Sgm By) . j)) by A1, A55, A8, A53, A54, A60, A58
.= (Segm (M,Bx,By)) * (i,j) by A56, MATRIX13:def 1 ;
:: thesis:

end;

hence Segm (M,Bx,By) = B by MATRIX_0:27; :: thesis:
set MC = Segm (M,Cx,Cy);
A61: dom (Sgm Cy) = Seg (card Cy) by A11, FINSEQ_3:40;
A62: dom (Sgm Cx) = Seg (card Cx) by A14, FINSEQ_3:40;

now :: thesis:

let i, j be Nat; :: thesis:
assume A63: [i,j] in Indices (Segm (M,Cx,Cy)) ; :: thesis:
card Cx <> 0 by A63, MATRIX_0:22;
then A64: Indices (Segm (M,Cx,Cy)) = [:(Seg (card Cx)),(Seg (card Cy)):] by MATRIX_0:23;
then A65: j in Seg (card Cy) by A63, ZFMISC_1:87;
then A66: (Sgm Cy) . j in Cy by A12, A61, FUNCT_1:def 3;
A67: i in Seg (card Cx) by A63, A64, ZFMISC_1:87;
then (Sgm Cx) . i in Cx by A15, A62, FUNCT_1:def 3;
then [((Sgm Cx) . i),((Sgm Cy) . j)] in [:Cx,Cy:] by A66, ZFMISC_1:87;
hence C * (i,j) = M * (((Sgm Cx) . i),((Sgm Cy) . j)) by A2, A62, A61, A53, A54, A67, A65
.= (Segm (M,Cx,Cy)) * (i,j) by A63, MATRIX13:def 1 ;
:: thesis:

end;

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