let E be non empty set ; :: thesis: for e being El_ev of E ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
let e be El_ev of E; :: thesis: ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
consider a being Element of E such that
A1: ( a in E & e = {a} ) by Th11;
reconsider p = <*a*> as FinSequence ;
A2: rng p = {a} by FINSEQ_1:56;
len p = 1 by FINSEQ_1:56;
hence ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 ) by A1, A2; :: thesis: verum