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: for i, j being Nat st [i,j] in [:(Seg (len A)),(Seg (width A)):] holds
for x1, x2 being Element of D st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2

let i, j be Nat; :: thesis:
assume [i,j] in [:(Seg (len A)),(Seg (width A)):] ; :: thesis:
let x1, x2 be Element of D; :: thesis:
assume that
A7: S₁[i,j,x1] and
A8: S₁[i,j,x2] ; :: thesis:

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

suppose A9: [i,j] in [:Bx,By:] ; :: thesis:

then consider m, n being Nat such that
A10: ( m in dom (Sgm Bx) & n in dom (Sgm By) & (Sgm Bx) . m = i & (Sgm By) . n = j ) by A7;
thus x1 = B * m,n by A7, A9, A10
.= x2 by A8, A9, A10 ; :: thesis:

end;

suppose A11: [i,j] in [:Cx,Cy:] ; :: thesis:

then consider m, n being Nat such that
A12: ( m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j ) by A7;
thus x1 = C * m,n by A7, A11, A12
.= x2 by A8, A11, A12 ; :: thesis:

end;

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

then A13: not [i,j] in [:Bx,By:] \/ [:Cx,Cy:] by XBOOLE_0:def 3;
hence x1 = A * i,j by A7
.= x2 by A8, A13 ;
:: thesis:

end;

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:45;
A17: Sgm By is one-to-one by A4, FINSEQ_3:99;
A18: Sgm Bx is one-to-one by A14, FINSEQ_3:99;
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:99;
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:99;
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]

proof

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:106;
then consider yC being set such that
A27: yC in dom (Sgm Cy) and
A28: (Sgm Cy) . yC = j by A20, FUNCT_1:def 5;
j in By by A26, ZFMISC_1:106;
then consider y being set such that
A29: y in dom (Sgm By) and
A30: (Sgm By) . y = j by A5, FUNCT_1:def 5;
i in Cx by A26, ZFMISC_1:106;
then consider xC being set such that
A31: xC in dom (Sgm Cx) and
A32: (Sgm Cx) . xC = i by A23, FUNCT_1:def 5;
i in Bx by A26, ZFMISC_1:106;
then consider x being set such that
A33: x in dom (Sgm Bx) and
A34: (Sgm Bx) . x = i by A15, FUNCT_1:def 5;
reconsider x = x, y = y, xC = xC, yC = yC as Element of NAT by A33, A29, A31, A27;
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:54;
A37: ((Sgm By) " ) . j = y by A17, A29, A30, FUNCT_1:54;
( [i,j] in [:Bx,By:] /\ [:Cx,Cy:] & ((Sgm Bx) " ) . i = x ) by A18, A26, A33, A34, FUNCT_1:54, 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 8;
hence BB = B * m,n by A17, A29, A30, A39, A41, FUNCT_1:def 8; :: 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:106;
then consider y being set such that
A43: y in dom (Sgm By) and
A44: (Sgm By) . y = j by A5, FUNCT_1:def 5;
i in Bx by A42, ZFMISC_1:106;
then consider x being set such that
A45: x in dom (Sgm Bx) and
A46: (Sgm Bx) . x = i by A15, FUNCT_1:def 5;
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 8;
hence BB = B * m,n by A17, A43, A44, A48, A50, FUNCT_1:def 8; :: 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:106;
then consider y being set such that
A52: y in dom (Sgm Cy) and
A53: (Sgm Cy) . y = j by A20, FUNCT_1:def 5;
i in Cx by A51, ZFMISC_1:106;
then consider x being set such that
A54: x in dom (Sgm Cx) and
A55: (Sgm Cx) . x = i by A23, FUNCT_1:def 5;
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 8;
hence CC = C * m,n by A21, A52, A53, A57, A59, FUNCT_1:def 8; :: 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 AA = A * i,j; :: thesis:
thus S₁[i,j,AA] 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(A6, 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:27;
A63: dom (Sgm Bx) = Seg (card Bx) by A14, FINSEQ_3:45;

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:23;
then A65: Indices (Segm M,Bx,By) = [:(Seg (card Bx)),(Seg (card By)):] by MATRIX_1:24;
then A66: j in Seg (card By) by A64, ZFMISC_1:106;
then A67: (Sgm By) . j in By by A5, A16, FUNCT_1:def 5;
A68: i in Seg (card Bx) by A64, A65, ZFMISC_1:106;
then (Sgm Bx) . i in Bx by A15, A63, FUNCT_1:def 5;
then [((Sgm Bx) . i),((Sgm By) . j)] in [:Bx,By:] by A67, ZFMISC_1:106;
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:28; :: thesis:
set MC = Segm M,Cx,Cy;
A69: dom (Sgm Cy) = Seg (card Cy) by A19, FINSEQ_3:45;
A70: dom (Sgm Cx) = Seg (card Cx) by A22, FINSEQ_3:45;

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:23;
then A72: Indices (Segm M,Cx,Cy) = [:(Seg (card Cx)),(Seg (card Cy)):] by MATRIX_1:24;
then A73: j in Seg (card Cy) by A71, ZFMISC_1:106;
then A74: (Sgm Cy) . j in Cy by A20, A69, FUNCT_1:def 5;
A75: i in Seg (card Cx) by A71, A72, ZFMISC_1:106;
then (Sgm Cx) . i in Cx by A23, A70, FUNCT_1:def 5;
then [((Sgm Cx) . i),((Sgm Cy) . j)] in [:Cx,Cy:] by A74, ZFMISC_1:106;
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:28; :: 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: