let y be object ; :: 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} and
A3: rng g = {y} ; :: thesis: f = g
for x being object st x in dom f holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume A4: x in dom f ; :: thesis: f . x = g . x
then f . x in rng f by Def3;
then A5: f . x = y by A2, TARSKI:def 1;
g . x in rng g by A1, A4, Def3;
hence f . x = g . x by A3, A5, TARSKI:def 1; :: thesis: verum

end;

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