let G1, G2, G3 be Ring; :: thesis: ( G1 <= G2 & G2 <= G3 implies G1 <= G3 )
assume A1: ( G1 <= G2 & G2 <= G3 ) ; :: thesis: G1 <= G3
then consider F0 being RingMorphism such that
A2: ( dom F0 = G1 & cod F0 = G2 ) by Def8;
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 A2;
then reconsider F' = F as Morphism of G1,G2 by A1, Def9;
consider G0 being RingMorphism such that
A3: ( dom G0 = G2 & cod G0 = G3 ) by A1, Def8;
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 A3;
then reconsider G' = G as Morphism of G2,G3 by A1, Def9;
consider g being Function of G2,G3 such that
A4: G' = RingMorphismStr(# G2,G3,g #) by A1, Lm8;
consider f being Function of G1,G2 such that
A5: F' = RingMorphismStr(# G1,G2,f #) by A1, Lm8;
dom G = cod F by A2, A3;
then G * F = RingMorphismStr(# G1,G3,(g * f) #) by A4, A5, Def10;
then ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
hence G1 <= G3 by Def8; :: thesis: verum