take E ; :: thesis: ( E is E -homomorphic & E is E -monomorphic & E is F -homomorphic & E is F -monomorphic )
id E is RingHomomorphism ;
hence E is E -homomorphic by RING_2:def 4; :: thesis: ( E is E -monomorphic & E is F -homomorphic & E is F -monomorphic )
( id E is RingHomomorphism & id E is monomorphism ) ;
hence E is E -monomorphic by RING_3:def 3; :: thesis: ( E is F -homomorphic & E is F -monomorphic )
thus E is F -homomorphic ; :: thesis: E is F -monomorphic
thus E is F -monomorphic ; :: thesis: verum