let f be Function; :: thesis: ( f = <*x*> iff ( dom f = Seg 1 & f . 1 = x ) )

hereby :: thesis: ( dom f = Seg 1 & f . 1 = x implies f = <*x*> )

assume A1: f = <*x*> ; :: thesis: ( dom f = Seg 1 & f . 1 = x )
hence dom f = Seg 1 by Th4, RELAT_1:23; :: thesis: f . 1 = x
[1,x] in f by A1, TARSKI:def 1;
hence f . 1 = x by FUNCT_1:8; :: thesis: verum

end;

assume A2: ( dom f = Seg 1 & f . 1 = x ) ; :: thesis: f = <*x*>
reconsider g = {[1,(f . 1)]} as Function ;
f = {[1,(f . 1)]}

proof

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 [y,z] in f ; :: thesis: [y,z] in g
then ( y in {1} & z in rng f & rng f = {(f . 1)} ) by A2, Th4, FUNCT_1:14, RELAT_1:def 4, RELAT_1:def 5;
then ( y = 1 & z = f . 1 ) by TARSKI:def 1;
hence [y,z] in g by TARSKI:def 1; :: thesis: verum

end;

assume [y,z] in g ; :: thesis: [y,z] in f
then ( y = 1 & z = f . 1 & 1 in dom f ) by A2, Lm5;
hence [y,z] in f by FUNCT_1:def 4; :: thesis: verum

end;

hence f = {[1,(f . 1)]} by RELAT_1:def 2; :: thesis: verum

end;

hence f = <*x*> by A2; :: thesis: verum