functor (K : Field.T-> Ring.T