let F be RingMorphism; :: thesis: ex G, H being Ring st
( G <= H & dom F = G & cod F = H & RingMorphismStr(# the DomR of F, the CodR of F, the Fun of F #) is Morphism of G,H )
reconsider S = RingMorphismStr(# the DomR of F, the CodR of F, the Fun of F #) as RingMorphism by Lm2;
set G = the DomR of F;
set H = the CodR of F;
take the DomR of F ; :: thesis: ex H being Ring st
( the DomR of F <= H & dom F = the DomR of F & cod F = H & RingMorphismStr(# the DomR of F, the CodR of F, the Fun of F #) is Morphism of the DomR of F,H )
take the CodR of F ; :: thesis: ( the DomR of F <= the CodR of F & dom F = the DomR of F & cod F = the CodR of F & RingMorphismStr(# the DomR of F, the CodR of F, the Fun of F #) is Morphism of the DomR of F, the CodR of F )
( dom F = the DomR of F & cod F = the CodR of F ) ;
then A1: the DomR of F <= the CodR of F ;
( dom S = the DomR of F & cod S = the CodR of F ) ;
hence ( the DomR of F <= the CodR of F & dom F = the DomR of F & cod F = the CodR of F & RingMorphismStr(# the DomR of F, the CodR of F, the Fun of F #) is Morphism of the DomR of F, the CodR of F ) by A1, Def8; :: thesis: verum