let F be strict RingMorphism; :: thesis: ( F is Morphism of dom F, cod F & dom F <= cod F )
ex G, H being Ring st
( G <= H & dom F = G & cod F = H & F is Morphism of G,H ) by Lm6;
hence ( F is Morphism of dom F, cod F & dom F <= cod F ) ; :: thesis: verum