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 A1: ( [:Bx,By:] c= Indices A & [:Cx,Cy:] c= Indices A ) ; :: thesis:
set bx = card Bx;
set bY = card By;
set cx = card Cx;
set cy = card Cy;
set l = len A;
set w = width A;
let B be Matrix of card Bx, card By,D; :: thesis:
let C be Matrix of card Cx, card Cy,D; :: thesis:
assume A2: 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:
consider kBx being Nat such that
A3: Bx c= Seg kBx by MATRIX13:43;
consider kBy being Nat such that
A4: By c= Seg kBy by MATRIX13:43;
consider kCx being Nat such that
A5: Cx c= Seg kCx by MATRIX13:43;
consider kCy being Nat such that
A6: Cy c= Seg kCy by MATRIX13:43;
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 ) );
A7: 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

proof

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 A8: ( S₁[i,j,x1] & 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) ) and
A11: ( (Sgm Bx) . m = i & (Sgm By) . n = j ) by A8;
thus x1 = B * m,n by A8, A9, A10, A11
.= x2 by A8, A9, A10, A11 ; :: thesis:

end;

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

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

end;

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

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

end;

A16: ( rng (Sgm Bx) = Bx & rng (Sgm By) = By & dom (Sgm Bx) = Seg (card Bx) & dom (Sgm By) = Seg (card By) & rng (Sgm Cx) = Cx & rng (Sgm Cy) = Cy & dom (Sgm Cx) = Seg (card Cx) & dom (Sgm Cy) = Seg (card Cy) & Sgm Bx is one-to-one & Sgm By is one-to-one & Sgm Cx is one-to-one & Sgm Cy is one-to-one ) by A3, A4, A5, A6, FINSEQ_1:def 13, FINSEQ_3:45, FINSEQ_3:99;
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]

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 A18: ( [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) ; :: thesis:

then i in Bx by ZFMISC_1:106;
then consider x being set such that
A19: ( x in dom (Sgm Bx) & (Sgm Bx) . x = i ) by A16, FUNCT_1:def 5;
j in By by A18, ZFMISC_1:106;
then consider y being set such that
A20: ( y in dom (Sgm By) & (Sgm By) . y = j ) by A16, FUNCT_1:def 5;
i in Cx by A18, ZFMISC_1:106;
then consider xC being set such that
A21: ( xC in dom (Sgm Cx) & (Sgm Cx) . xC = i ) by A16, FUNCT_1:def 5;
j in Cy by A18, ZFMISC_1:106;
then consider yC being set such that
A22: ( yC in dom (Sgm Cy) & (Sgm Cy) . yC = j ) by A16, FUNCT_1:def 5;
reconsider x = x, y = y, xC = xC, yC = yC as Element of NAT by A19, A20, A21, A22;
take BB = B * x,y; :: thesis:

A23: now

let m, n be Nat; :: thesis:
assume that
A24: ( m in dom (Sgm Bx) & n in dom (Sgm By) ) and
A25: ( (Sgm Bx) . m = i & (Sgm By) . n = j ) ; :: thesis:
( x = m & y = n ) by A16, A19, A20, A24, A25, FUNCT_1:def 8;
hence BB = B * m,n ; :: thesis:

end;

A26: now

let m, n be Nat; :: thesis:
assume that
A27: ( m in dom (Sgm Cx) & n in dom (Sgm Cy) ) and
A28: ( (Sgm Cx) . m = i & (Sgm Cy) . n = j ) ; :: thesis:
A29: [i,j] in [:Bx,By:] /\ [:Cx,Cy:] by A18, XBOOLE_0:def 4;
( ((Sgm Bx) " ) . i = x & ((Sgm By) " ) . j = y & ((Sgm Cx) " ) . i = m & ((Sgm Cy) " ) . j = n ) by A16, A19, A20, A27, A28, FUNCT_1:54;
hence BB = C * m,n by A2, A29; :: thesis:

end;

( xC in dom (Sgm Cx) & (Sgm Cx) . xC = i & yC in dom (Sgm Cy) & (Sgm Cy) . yC = j ) by A21, A22;
hence S₁[i,j,BB] by A19, A20, A23, A26, A18, XBOOLE_0:def 3; :: thesis:

end;

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

then i in Bx by ZFMISC_1:106;
then consider x being set such that
A31: ( x in dom (Sgm Bx) & (Sgm Bx) . x = i ) by A16, FUNCT_1:def 5;
j in By by A30, ZFMISC_1:106;
then consider y being set such that
A32: ( y in dom (Sgm By) & (Sgm By) . y = j ) by A16, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A31, A32;
take BB = B * x,y; :: thesis:

now

let m, n be Nat; :: thesis:
assume that
A33: ( m in dom (Sgm Bx) & n in dom (Sgm By) ) and
A34: ( (Sgm Bx) . m = i & (Sgm By) . n = j ) ; :: thesis:
( x = m & y = n ) by A16, A31, A32, A33, A34, FUNCT_1:def 8;
hence BB = B * m,n ; :: thesis:

end;

hence S₁[i,j,BB] by A31, A32, A30, XBOOLE_0:def 3; :: thesis:

end;

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

then i in Cx by ZFMISC_1:106;
then consider x being set such that
A36: ( x in dom (Sgm Cx) & (Sgm Cx) . x = i ) by A16, FUNCT_1:def 5;
j in Cy by A35, ZFMISC_1:106;
then consider y being set such that
A37: ( y in dom (Sgm Cy) & (Sgm Cy) . y = j ) by A16, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A36, A37;
take CC = C * x,y; :: thesis:

now

let m, n be Nat; :: thesis:
assume that
A38: ( m in dom (Sgm Cx) & n in dom (Sgm Cy) ) and
A39: ( (Sgm Cx) . m = i & (Sgm Cy) . n = j ) ; :: thesis:
( x = m & y = n ) by A16, A36, A37, A38, A39, FUNCT_1:def 8;
hence CC = C * m,n ; :: thesis:

end;

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

end;

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

end;

consider M being Matrix of len A, width A,D such that
A41: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * i,j] from MATRIX_1:sch 2(A7, A17);
take M ; :: thesis:
set MB = Segm M,Bx,By;
A is Matrix of len A, width A,D by MATRIX_2:7;
then A42: ( Indices A = Indices M & Indices (Segm M,Bx,By) = Indices B ) by MATRIX_1:27;

now

let i, j be Nat; :: thesis:
assume A43: [i,j] in Indices (Segm M,Bx,By) ; :: thesis:
card Bx <> 0 by A43, MATRIX_1:23;
then card Bx > 0 ;
then Indices (Segm M,Bx,By) = [:(Seg (card Bx)),(Seg (card By)):] by MATRIX_1:24;
then A44: ( i in Seg (card Bx) & j in Seg (card By) ) by A43, ZFMISC_1:106;
then ( (Sgm Bx) . i in Bx & (Sgm By) . j in By ) by A16, FUNCT_1:def 5;
then [((Sgm Bx) . i),((Sgm By) . j)] in [:Bx,By:] by ZFMISC_1:106;
hence B * i,j = M * ((Sgm Bx) . i),((Sgm By) . j) by A1, A16, A41, A42, A44
.= (Segm M,Bx,By) * i,j by A43, MATRIX13:def 1 ;
:: thesis:

end;

hence Segm M,Bx,By = B by MATRIX_1:28; :: thesis:
set MC = Segm M,Cx,Cy;

now

let i, j be Nat; :: thesis:
assume A45: [i,j] in Indices (Segm M,Cx,Cy) ; :: thesis:
card Cx <> 0 by A45, MATRIX_1:23;
then card Cx > 0 ;
then Indices (Segm M,Cx,Cy) = [:(Seg (card Cx)),(Seg (card Cy)):] by MATRIX_1:24;
then A46: ( i in Seg (card Cx) & j in Seg (card Cy) ) by A45, ZFMISC_1:106;
then ( (Sgm Cx) . i in Cx & (Sgm Cy) . j in Cy ) by A16, FUNCT_1:def 5;
then [((Sgm Cx) . i),((Sgm Cy) . j)] in [:Cx,Cy:] by ZFMISC_1:106;
hence C * i,j = M * ((Sgm Cx) . i),((Sgm Cy) . j) by A1, A16, A41, A42, A46
.= (Segm M,Cx,Cy) * i,j by A45, MATRIX13:def 1 ;
:: thesis:

end;

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