theorem Th36: :: TOPS_5:36

for f being non-empty Function
for X being set
for i being object st i in dom f holds
( product (f +* (i,X)) = {} iff X is empty )