Op-Right (f,n) = f /^ n ;
hence Op-Right (f,n) is FinSequence of D ; :: thesis: verum