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