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

proof

assume A1: p = <%x%> ; :: thesis: ( dom p = Segm 1 & rng p = {x} )
hence dom p = Segm 1 by Def4; :: thesis: rng p = {x}
rng p = {(p . 0)} by FUNCT_1:4, A1;
hence rng p = {x} by A1, Def4; :: thesis: verum

end;

assume that
A2: dom p = Segm 1 and
A3: rng p = {x} ; :: thesis: p = <%x%>
1 = 0 + 1 ;
then p . 0 in {x} by A2, A3, FUNCT_1:3, NAT_1:45;
then p . 0 = x by TARSKI:def 1;
hence p = <%x%> by A2, Def4; :: thesis: verum