let y be set ; :: thesis: for f, g being Function st dom f = dom g & rng f = {y} & rng g = {y} holds
f = g
let f, g be Function; :: thesis: ( dom f = dom g & rng f = {y} & rng g = {y} implies f = g )
assume that
A1: dom f = dom g and
A2: ( rng f = {y} & rng g = {y} ) ; :: thesis: f = g
for x being set st x in dom f holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then ( f . x in rng f & g . x in rng g ) by A1, Def5;
then ( f . x = y & g . x = y ) by A2, TARSKI:def 1;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A1, Th9; :: thesis: verum