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

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