theorem :: PARTFUN1:18

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