theorem :: FINSEQ_3:116

for f being FinSubsequence st f is FinSequence holds
Seq f = f