theorem Th38: :: TOPS_5:38

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