theorem Th100: :: FUNCT_4:100

for f being Function
for x, y being object st x <> y holds
not x in rng (f +~ (x,y))