thus s * N is subsequence of s by Def17; :: thesis: