let G1, G2, G3 be Ring; :: thesis: ( G1 <= G2 & G2 <= G3 implies G1 <= G3 )
assume that
A1: G1 <= G2 and
A2: G2 <= G3 ; :: thesis: 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 ; :: thesis: verum