let p be Function; :: thesis: ( p is FinSequence-like implies p is FinSubsequence-like )
assume p is FinSequence-like ; :: thesis: p is FinSubsequence-like
then reconsider p = p as FinSequence ;
dom p = Seg (len p) by Def3;
hence p is FinSubsequence-like by Def12; :: thesis: verum