let F be RingMorphism; 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
; 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
; ( 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; verum