let Y be set ; :: thesis: for x being object
for f being Function of {x},Y st Y <> {} holds
f . x in Y
let x be object ; :: 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 A1: dom f = {x} by Def1;
rng f c= Y ;
then {(f . x)} c= Y by A1, FUNCT_1:4;
hence f . x in Y by ZFMISC_1:31; :: thesis: verum