theorem Th39: :: TOPS_5:39

for f being Function
for X being set
for i being object st i in dom f & X c= f . i holds
product (f +* (i,X)) c= product f