let x, Y be set ; :: thesis: for f being Function of {x},Y st Y <> {} holds
rng f = {(f . x)}
let f be Function of {x},Y; :: thesis: ( Y <> {} implies rng f = {(f . x)} )
assume Y <> {} ; :: thesis: rng f = {(f . x)}
then dom f = {x} by Def1;
hence rng f = {(f . x)} by FUNCT_1:14; :: thesis: verum