let x be object ; for f being Function st dom f = {x} holds
f = {[x,(f . x)]}
let f be Function; ( dom f = {x} implies f = {[x,(f . x)]} )
reconsider g = {[x,(f . x)]} as Function ;
assume A1:
dom f = {x}
; 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 ;
( [y,z] in f iff [y,z] in g )
thus
(
[y,z] in f implies
[y,z] in g )
( [y,z] in g implies [y,z] in f )
assume
[y,z] in g
;
[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;
verum
end;
hence
f = {[x,(f . x)]}
; verum