let f be FinSequence; :: thesis: f ^' {} = f
thus f ^' {} = f ^ {} by Def1
.= f by FINSEQ_1:34 ; :: thesis: verum