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