theorem Th16: :: PARTFUN1:16

for x being object
for Y being set
for f being PartFunc of {x},Y holds rng f c= {(f . x)}