let f be Function; :: thesis: ( 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; :: thesis: ( dom f = 1 & f . 0 = x implies f = <%x%> )
assume that
A1: dom f = 1 and
A2: f . 0 = x ; :: thesis: 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 ; :: thesis: ( [y,z] in f iff [y,z] in g )

hereby :: thesis: ( [y,z] in g implies [y,z] in f )

assume A3: [y,z] in f ; :: thesis: [y,z] in g
then 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; :: thesis: verum

end;

assume [y,z] in g ; :: thesis: [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; :: thesis: verum

end;

then f = {[0,(f . 0)]} ;
hence f = <%x%> by A2, FUNCT_4:82; :: thesis: verum