theorem Th30: :: TOPS_5:30

for f being non-empty Function
for X, Y being set
for i, j, x, y being object
for g being Function st x in X & y in Y & i <> j & g in product f holds
g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y)))