theorem :: TOPS_5:41

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