let G2, G3, G1 be Ring; :: thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds
G * F is Morphism of G1,G3
let G be Morphism of G2,G3; :: thesis: for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds
G * F is Morphism of G1,G3
let F be Morphism of G1,G2; :: thesis: ( G1 <= G2 & G2 <= G3 implies G * F is Morphism of G1,G3 )
assume A1: ( G1 <= G2 & G2 <= G3 ) ; :: thesis: G * F is Morphism of G1,G3
then consider g being Function of G2,G3 such that
A2: G = RingMorphismStr(# G2,G3,g #) by Lm8;
consider f being Function of G1,G2 such that
A3: F = RingMorphismStr(# G1,G2,f #) by A1, Lm8;
dom G = G2 by A1, Def9
.= cod F by A1, Def9 ;
then G * F = RingMorphismStr(# G1,G3,(g * f) #) by A2, A3, Def10;
then A4: ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
G1 <= G3 by A1, Th8;
hence G * F is Morphism of G1,G3 by A4, Def9; :: thesis: verum