let p be FinSequence; :: thesis: for x being object holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )
let x be object ; :: 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