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