let x be set ; :: thesis: for f being FinSequence holds f ^' <*x*> = f
let f be FinSequence; :: thesis: f ^' <*x*> = f
len <*x*> = 1 by FINSEQ_1:39;
then (2,(len <*x*>)) -cut <*x*> = {} by Def1;
hence f ^' <*x*> = f by FINSEQ_1:34; :: thesis: verum