theorem Th9: :: MATRIX15:9

for D being non empty set
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) ) )