theorem Th27: :: TOPS_5:27

for f being Function
for X, Y being set
for i being object st X c= Y holds
product (f +* (i .--> X)) c= product (f +* (i .--> Y))