let G1, G2, G3 be Ring; ( G1 <= G2 & G2 <= G3 implies G1 <= G3 )
assume that
A1:
G1 <= G2
and
A2:
G2 <= G3
; G1 <= G3
consider F0 being RingMorphism such that
A3:
dom F0 = G1
and
A4:
cod F0 = G2
by A1;
reconsider F = RingMorphismStr(# the Dom of F0, the Cod of F0, the Fun of F0 #) as RingMorphism by Lm2;
( dom F = G1 & cod F = G2 )
by A3, A4;
then reconsider F9 = F as Morphism of G1,G2 by A1, Def8;
consider f being Function of G1,G2 such that
A5:
F9 = RingMorphismStr(# G1,G2,f #)
by A1, Lm8;
consider G0 being RingMorphism such that
A6:
dom G0 = G2
and
A7:
cod G0 = G3
by A2;
reconsider G = RingMorphismStr(# the Dom of G0, the Cod of G0, the Fun of G0 #) as RingMorphism by Lm2;
( dom G = G2 & cod G = G3 )
by A6, A7;
then reconsider G9 = G as Morphism of G2,G3 by A2, Def8;
consider g being Function of G2,G3 such that
A8:
G9 = RingMorphismStr(# G2,G3,g #)
by A2, Lm8;
dom G = cod F
by A4, A6;
then
G * F = RingMorphismStr(# G1,G3,(g * f) #)
by A8, A5, Def9;
then
( dom (G * F) = G1 & cod (G * F) = G3 )
;
hence
G1 <= G3
; verum