theorem Th37: :: TOPS_5:37

for f being non-empty Function
for X being set
for i, x being object
for g being Function st i in dom f & x in X & g in product f holds
g +* (i,x) in product (f +* (i,X))