let a be set ; :: thesis: for f being FinSequence st f = <*a*> holds
f | 1 = <*a*>
let f be FinSequence; :: thesis: ( f = <*a*> implies f | 1 = <*a*> )
assume A1: f = <*a*> ; :: thesis: f | 1 = <*a*>
then len f <= 1 by FINSEQ_1:40;
hence f | 1 = <*a*> by A1, FINSEQ_1:58; :: thesis: verum