let x be object ; :: thesis: for f being Function st dom f = {x} holds
f = {[x,(f . x)]}
let f be Function; :: thesis: ( dom f = {x} implies f = {[x,(f . x)]} )
reconsider g = {[x,(f . x)]} as Function ;
assume A1: dom f = {x} ; :: thesis: f = {[x,(f . x)]}
for y, z being object holds
( [y,z] in f iff [y,z] in g )
proof
let y, z be object ; :: thesis: ( [y,z] in f iff [y,z] in g )
thus ( [y,z] in f implies [y,z] in g ) :: thesis: ( [y,z] in g implies [y,z] in f )
proof
assume A2: [y,z] in f ; :: thesis: [y,z] in g
then y in {x} by A1, XTUPLE_0:def 12;
then A3: y = x by TARSKI:def 1;
A4: rng f = {(f . x)} by A1, FUNCT_1:4;
z in rng f by A2, XTUPLE_0:def 13;
then z = f . x by A4, TARSKI:def 1;
hence [y,z] in g by A3, TARSKI:def 1; :: thesis: verum
end;
assume [y,z] in g ; :: thesis: [y,z] in f
then A5: ( y = x & z = f . x ) by Lm2;
x in dom f by A1, TARSKI:def 1;
hence [y,z] in f by A5, FUNCT_1:def 2; :: thesis: verum
end;
hence f = {[x,(f . x)]} ; :: thesis: verum