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:87, FUNCOP_1:19, FUNCOP_1:87; :: 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 set holds
( [y,z] in f iff [y,z] in g )

proof

let y, z be set ; :: 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:87, RELAT_1:def 4;
then A4: y = 0 by TARSKI:def 1;
A5: rng f = {(f . 0 )} by A1, CARD_1:87, FUNCT_1:14;
z in rng f by A3, RELAT_1:def 5;
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 Lm1;
0 in dom f by A1, CARD_1:87, TARSKI:def 1;
hence [y,z] in f by A6, FUNCT_1:def 4; :: thesis: verum

end;

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