let f be FinSubsequence; :: thesis: ( f is FinSequence implies Seq f = f )
assume f is FinSequence ; :: thesis: Seq f = f
then reconsider ss9 = f as FinSequence ;
consider k being Nat such that
A1: dom ss9 = Seg k by FINSEQ_1:def 2;
k in NAT by ORDINAL1:def 12;
then A2: len ss9 <= k by A1, FINSEQ_1:def 3;
Seq f = f * (Sgm (Seg k)) by A1, FINSEQ_1:def 14
.= f * (idseq k) by Th46
.= f by A2, FINSEQ_2:54 ;
hence Seq f = f ; :: thesis: verum