let f be Function; :: thesis: for x being object st rng f = {x} holds
f = (dom f) --> x
let x be object ; :: thesis: ( rng f = {x} implies f = (dom f) --> x )
assume A1: rng f = {x} ; :: thesis: f = (dom f) --> x
then dom f <> {} by RELAT_1:42;
then ( dom ((dom f) --> x) = dom f & rng ((dom f) --> x) = {x} ) by RELAT_1:160;
hence f = (dom f) --> x by A1, FUNCT_1:7; :: thesis: verum