let x be set ; :: thesis: for p being FinSequence holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )
let p be FinSequence; :: 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}
dom p = {1} by A1, Def8, Th4;
then rng p = {(p . 1)} by FUNCT_1:4;
hence rng p = {x} by A1, Def8; :: 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