let S be Ring; :: thesis: ( S is R -monomorphic implies S is n -characteristic )
assume A1: S is R -monomorphic ; :: thesis: S is n -characteristic
Char R = n by Def6;
hence S is n -characteristic by A1, Th87; :: thesis: verum