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

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