let x be object ; :: thesis: for P, Y being set
for f being PartFunc of {x},Y holds f .: P c= {(f . x)}
let P, Y be set ; :: thesis: for f being PartFunc of {x},Y holds f .: P c= {(f . x)}
let f be PartFunc of {x},Y; :: thesis: f .: P c= {(f . x)}
( f .: P c= rng f & rng f c= {(f . x)} ) by Th16, RELAT_1:111;
hence f .: P c= {(f . x)} ; :: thesis: verum