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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 S_{1}[ 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_{1}[i,j,x]

A53: for i, j being Nat st [i,j] in Indices M holds

S_{1}[i,j,M * (i,j)]
from MATRIX_0:sch 2(A17);

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 (Indices M) \ ([: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 A6, FINSEQ_3:40;

M * (i,j) = A * (i,j) ) )

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;

M * (i,j) = A * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) implies M * (i,j) = A * (i,j) )

assume A68: [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) ; :: thesis: M * (i,j) = A * (i,j)

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: verum

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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 (Indices M) \ ([: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 S

( ( [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

proof

consider M being Matrix of len A, width A,D such that
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (len A)),(Seg (width A)):] implies ex x being Element of D st S_{1}[i,j,x] )

assume [i,j] in [:(Seg (len A)),(Seg (width A)):] ; :: thesis: ex x being Element of D st S_{1}[i,j,x]

end;assume [i,j] in [:(Seg (len A)),(Seg (width A)):] ; :: thesis: ex x being Element of D st S

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:] ) )
;

end;

suppose A18:
( [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] )
; :: thesis: ex x being Element of D st S_{1}[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 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: S_{1}[i,j,BB]

_{1}[i,j,BB]
by A18, A25, A26, A21, A22, A23, A24, A19, A20, A27, XBOOLE_0:def 3; :: thesis: verum

end;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: S

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)

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 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: verum

end;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 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: verum

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)

hence
SBB = 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 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: verum

end;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 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: verum

suppose A34:
( [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:] )
; :: thesis: ex x being Element of D st S_{1}[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 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: S_{1}[i,j,BB]

_{1}[i,j,BB]
by A34, A37, A38, A35, A36, XBOOLE_0:def 3; :: thesis: verum

end;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: S

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)

hence
SBB = 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 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: verum

end;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 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: verum

suppose A43:
( not [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:] )
; :: thesis: ex x being Element of D st S_{1}[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 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: S_{1}[i,j,CC]

_{1}[i,j,CC]
by A43, A46, A47, A44, A45, XBOOLE_0:def 3; :: thesis: verum

end;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: S

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)

hence
SCC = 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 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: verum

end;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 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: verum

A53: for i, j being Nat st [i,j] in Indices M holds

S

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 (Indices M) \ ([: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 A6, FINSEQ_3:40;

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)

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 (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) 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 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: verum

end;assume A56: [i,j] in Indices (Segm (M,Bx,By)) ; :: thesis: B * (i,j) = (Segm (M,Bx,By)) * (i,j)

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: verum

M * (i,j) = A * (i,j) ) )

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: for i, j being Nat st [i,j] in Indices (Segm (M,Cx,Cy)) holds

C * (i,j) = (Segm (M,Cx,Cy)) * (i,j)

hence
Segm (M,Cx,Cy) = C
by MATRIX_0:27; :: thesis: for i, j being Nat st [i,j] in (Indices M) \ ([:Bx,By:] \/ [: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 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: verum

end;assume A63: [i,j] in Indices (Segm (M,Cx,Cy)) ; :: thesis: C * (i,j) = (Segm (M,Cx,Cy)) * (i,j)

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: verum

M * (i,j) = A * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) implies M * (i,j) = A * (i,j) )

assume A68: [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) ; :: thesis: M * (i,j) = A * (i,j)

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: verum