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 Th2, RELAT_1:9; :: thesis: f . 1 = x
[1,x] in f by A1, TARSKI:def 1;
hence f . 1 = x by FUNCT_1:1; :: thesis: verum

end;

assume that
A2: dom f = Seg 1 and
A3: f . 1 = x ; :: thesis: f = <*x*>
reconsider g = {[1,(f . 1)]} 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 A4: [y,z] in f ; :: thesis: [y,z] in g
then A5: y in {1} by A2, Th2, XTUPLE_0:def 12;
A6: z in rng f by A4, XTUPLE_0:def 13;
A7: rng f = {(f . 1)} by A2, Th2, FUNCT_1:4;
A8: y = 1 by A5, TARSKI:def 1;
z = f . 1 by A6, A7, TARSKI:def 1;
hence [y,z] in g by A8, TARSKI:def 1; :: thesis: verum

end;

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

end;

hence f = <*x*> by A3, RELAT_1:def 2; :: thesis: verum