let P, Y be set ; :: thesis: for x being object
for f being Function of {x},Y st Y <> {} holds
f .: P c= {(f . x)}
let x be object ; :: 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 Th47; :: thesis: verum