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

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