let p be FinSequence; :: thesis: for x being object holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )
let x be object ; :: thesis: ( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )
thus ( p = <*x*> implies ( dom p = Seg 1 & rng p = {x} ) ) :: thesis: ( dom p = Seg 1 & rng p = {x} implies p = <*x*> )

proof

assume A1: p = <*x*> ; :: thesis: ( dom p = Seg 1 & rng p = {x} )
hence dom p = Seg 1 by Def8; :: thesis: rng p = {x}
rng p = {(p . 1)} by A1, Def8, Th2, FUNCT_1:4;
hence rng p = {x} by A1; :: thesis: verum

end;

assume that
A2: dom p = Seg 1 and
A3: rng p = {x} ; :: thesis: p = <*x*>
1 in dom p by A2;
then p . 1 in {x} by A3, FUNCT_1:def 3;
then p . 1 = x by TARSKI:def 1;
hence p = <*x*> by A2, Def8; :: thesis: verum