Op-Left (f,n) = f | n ;
hence Op-Left (f,n) is FinSequence of D ; :: thesis: verum