theorem Th101: :: FUNCT_7:102

for F being Function
for x, y being object st x in dom F holds
y in rng (F +* (x,y))