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