take E ; :: thesis: E is E -homomorphic
( id E is additive & id E is multiplicative & id E is unity-preserving ) ;
hence E is E -homomorphic by RING_2:def 4; :: thesis: verum