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