let f be Function; ( f = <%x%> iff ( dom f = 1 & f . 0 = x ) )
thus
( f = <%x%> implies ( dom f = 1 & f . 0 = x ) )
by CARD_1:49, FUNCOP_1:72; ( dom f = 1 & f . 0 = x implies f = <%x%> )
assume that
A1:
dom f = 1
and
A2:
f . 0 = x
; f = <%x%>
reconsider g = {[0,(f . 0)]} as Function ;
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 )
hereby ( [y,z] in g implies [y,z] in f )
assume A3:
[y,z] in f
;
[y,z] in gthen
y in {0}
by A1, CARD_1:49, XTUPLE_0:def 12;
then A4:
y = 0
by TARSKI:def 1;
A5:
rng f = {(f . 0)}
by A1, CARD_1:49, FUNCT_1:4;
z in rng f
by A3, XTUPLE_0:def 13;
then
z = f . 0
by A5, TARSKI:def 1;
hence
[y,z] in g
by A4, TARSKI:def 1;
verum
end;
assume
[y,z] in g
;
[y,z] in f
then A6:
(
y = 0 &
z = f . 0 )
by Lm2;
0 in dom f
by A1, CARD_1:49, TARSKI:def 1;
hence
[y,z] in f
by A6, FUNCT_1:def 2;
verum
end;
then
f = {[0,(f . 0)]}
;
hence
f = <%x%>
by A2, FUNCT_4:82; verum