let D be non empty set ; :: thesis: for A being Matrix of D
for Bx, By, Cx, Cy being finite without_zero Subset of NAT st [:Bx,By:] c= Indices A & [:Cx,Cy:] c= Indices A holds
for B being Matrix of card Bx, card By,D
for C being Matrix of card Cx, card Cy,D st ( 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) ) holds
ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

let A be Matrix of D; :: thesis: for Bx, By, Cx, Cy being finite without_zero Subset of NAT st [:Bx,By:] c= Indices A & [:Cx,Cy:] c= Indices A holds
for B being Matrix of card Bx, card By,D
for C being Matrix of card Cx, card Cy,D st ( 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) ) holds
ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

let Bx, By, Cx, Cy be finite without_zero Subset of NAT; :: thesis: ( [:Bx,By:] c= Indices A & [:Cx,Cy:] c= Indices A implies for B being Matrix of card Bx, card By,D
for C being Matrix of card Cx, card Cy,D st ( 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) ) holds
ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) ) )

assume that
A1: [:Bx,By:] c= Indices A and
A2: [:Cx,Cy:] c= Indices A ; :: thesis: for B being Matrix of card Bx, card By,D
for C being Matrix of card Cx, card Cy,D st ( 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) ) holds
ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

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: for C being Matrix of card Cx, card Cy,D st ( 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) ) holds
ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

let C be Matrix of card Cx, card Cy,D; :: thesis: ( ( 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) ) implies ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) ) )

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: ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

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 S1[ 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 ;
A9: Sgm By is one-to-one by ;
A10: Sgm Bx is one-to-one by ;
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 ;
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 ;
A17: for i, j being Nat st [i,j] in [:(Seg (len A)),(Seg ()):] holds
ex x being Element of D st S1[i,j,x]
proof
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (len A)),(Seg ()):] implies ex x being Element of D st S1[i,j,x] )
assume [i,j] in [:(Seg (len A)),(Seg ()):] ; :: thesis: ex x being Element of D st S1[i,j,x]
per cases ( ( [i,j] 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: ex x being Element of D st S1[i,j,x]
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 ;
j in By by ;
then consider y being object such that
A21: y in dom (Sgm By) and
A22: (Sgm By) . y = j by ;
i in Cx by ;
then consider xC being object such that
A23: xC in dom (Sgm Cx) and
A24: (Sgm Cx) . xC = i by ;
i in Bx by ;
then consider x being object such that
A25: x in dom (Sgm Bx) and
A26: (Sgm Bx) . x = i by ;
reconsider x = x, y = y as Element of NAT by ;
take BB = B * (x,y); :: thesis: S1[i,j,BB]
A27: now :: thesis: 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
BB = C * (m,n)
let m, n be Nat; :: thesis: ( m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j implies BB = C * (m,n) )
assume ( m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j ) ; :: thesis: BB = C * (m,n)
then A28: ( ((Sgm Cx) ") . i = m & ((Sgm Cy) ") . j = n ) by ;
A29: ((Sgm By) ") . j = y by ;
( [i,j] in [:Bx,By:] /\ [:Cx,Cy:] & ((Sgm Bx) ") . i = x ) by ;
hence BB = C * (m,n) by A3, A29, A28; :: thesis: verum
end;
now :: thesis: 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
BB = B * (m,n)
let m, n be Nat; :: thesis: ( m in dom (Sgm Bx) & n in dom (Sgm By) & (Sgm Bx) . m = i & (Sgm By) . n = j implies BB = B * (m,n) )
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: BB = B * (m,n)
x = m by ;
hence BB = B * (m,n) by ; :: thesis: verum
end;
hence S1[i,j,BB] by A18, A25, A26, A21, A22, A23, A24, A19, A20, A27, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A34: ( [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] ) ; :: thesis: ex x being Element of D st S1[i,j,x]
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 ;
i in Bx by ;
then consider x being object such that
A37: x in dom (Sgm Bx) and
A38: (Sgm Bx) . x = i by ;
reconsider x = x, y = y as Element of NAT by ;
take BB = B * (x,y); :: thesis: S1[i,j,BB]
now :: thesis: 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
BB = B * (m,n)
let m, n be Nat; :: thesis: ( m in dom (Sgm Bx) & n in dom (Sgm By) & (Sgm Bx) . m = i & (Sgm By) . n = j implies BB = B * (m,n) )
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: BB = B * (m,n)
x = m by ;
hence BB = B * (m,n) by ; :: thesis: verum
end;
hence S1[i,j,BB] by A34, A37, A38, A35, A36, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A43: ( not [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] ) ; :: thesis: ex x being Element of D st S1[i,j,x]
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 ;
i in Cx by ;
then consider x being object such that
A46: x in dom (Sgm Cx) and
A47: (Sgm Cx) . x = i by ;
reconsider x = x, y = y as Element of NAT by ;
take CC = C * (x,y); :: thesis: S1[i,j,CC]
now :: thesis: 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
CC = C * (m,n)
let m, n be Nat; :: thesis: ( m in dom (Sgm Cx) & n in dom (Sgm Cy) & (Sgm Cx) . m = i & (Sgm Cy) . n = j implies CC = C * (m,n) )
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: CC = C * (m,n)
x = m by ;
hence CC = C * (m,n) by ; :: thesis: verum
end;
hence S1[i,j,CC] by A43, A46, A47, A44, A45, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A52: ( not [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] ) ; :: thesis: ex x being Element of D st S1[i,j,x]
take A * (i,j) ; :: thesis: S1[i,j,A * (i,j)]
thus S1[i,j,A * (i,j)] by A52; :: thesis: verum
end;
end;
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
S1[i,j,M * (i,j)] from set MB = Segm (M,Bx,By);
take M ; :: thesis: ( Segm (M,Bx,By) = B & Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

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 ;
now :: thesis: for i, j being Nat st [i,j] in Indices (Segm (M,Bx,By)) holds
B * (i,j) = (Segm (M,Bx,By)) * (i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (M,Bx,By)) implies B * (i,j) = (Segm (M,Bx,By)) * (i,j) )
assume A56: [i,j] in Indices (Segm (M,Bx,By)) ; :: thesis: B * (i,j) = (Segm (M,Bx,By)) * (i,j)
card Bx <> 0 by ;
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 ;
then A59: (Sgm By) . j in By by ;
A60: i in Seg (card Bx) by ;
then (Sgm Bx) . i in Bx by ;
then [((Sgm Bx) . i),((Sgm By) . j)] in [:Bx,By:] by ;
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 ;
:: thesis: verum
end;
hence Segm (M,Bx,By) = B by MATRIX_0:27; :: thesis: ( Segm (M,Cx,Cy) = C & ( for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )

set MC = Segm (M,Cx,Cy);
A61: dom (Sgm Cy) = Seg (card Cy) by ;
A62: dom (Sgm Cx) = Seg (card Cx) by ;
now :: thesis: for i, j being Nat st [i,j] in Indices (Segm (M,Cx,Cy)) holds
C * (i,j) = (Segm (M,Cx,Cy)) * (i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (M,Cx,Cy)) implies C * (i,j) = (Segm (M,Cx,Cy)) * (i,j) )
assume A63: [i,j] in Indices (Segm (M,Cx,Cy)) ; :: thesis: C * (i,j) = (Segm (M,Cx,Cy)) * (i,j)
card Cx <> 0 by ;
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 ;
then A66: (Sgm Cy) . j in Cy by ;
A67: i in Seg (card Cx) by ;
then (Sgm Cx) . i in Cx by ;
then [((Sgm Cx) . i),((Sgm Cy) . j)] in [:Cx,Cy:] by ;
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 ;
:: thesis: verum
end;
hence Segm (M,Cx,Cy) = C by MATRIX_0:27; :: thesis: for i, j being Nat st [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) implies M * (i,j) = A * (i,j) )
assume A68: [i,j] in () \ ([:Bx,By:] \/ [:Cx,Cy:]) ; :: thesis: M * (i,j) = A * (i,j)
not [i,j] in [:Bx,By:] \/ [:Cx,Cy:] by ;
hence M * (i,j) = A * (i,j) by ; :: thesis: verum