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