theorem Th35: :: TOPS_5:35

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