let x, Y, P 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 Th69, RELAT_1:111;
hence f .: P c= {(f . x)} by XBOOLE_1:1; :: thesis: verum