let x be set ; :: thesis: for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & rng p = {x} ) )
let p be FinSequence; :: thesis: ( p = <*x*> iff ( len p = 1 & rng p = {x} ) )
( len p = 1 iff dom p = Seg 1 ) by Def3;
hence ( p = <*x*> iff ( len p = 1 & rng p = {x} ) ) by Th55; :: thesis: verum