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:56;
then 2,(len <*x*>) -cut <*x*> = {} by Def1;
hence f ^' <*x*> = f by FINSEQ_1:47; :: thesis: verum