take E ; :: thesis: E is E -monomorphic
( id E is additive & id E is multiplicative & id E is unity-preserving & id E is monomorphism ) ;
hence E is E -monomorphic by RING_3:def 3; :: thesis: verum