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