let x, Y, P be set ; :: thesis: for f being Function of {x},Y st Y <> {} holds
f .: P c= {(f . x)}
let f be Function of {x},Y; :: thesis: ( Y <> {} implies f .: P c= {(f . x)} )
f .: P c= rng f by RELAT_1:111;
hence ( Y <> {} implies f .: P c= {(f . x)} ) by Th62; :: thesis: verum