let E be non empty set ; :: thesis: for e being Singleton of E ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
let e be Singleton 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
a in E and
A1: e = {a} by Th6;
( rng <*a*> = {a} & len <*a*> = 1 ) by FINSEQ_1:39;
hence ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 ) by A1; :: thesis: verum