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 that
A1: G1 <= G2 and
A2: G2 <= G3 ; :: thesis: G * F is Morphism of G1,G3
consider g being Function of G2,G3 such that
A3: G = RingMorphismStr(# G2,G3,g #) by A2, Lm8;
consider f being Function of G1,G2 such that
A4: F = RingMorphismStr(# G1,G2,f #) by A1, Lm8;
dom G = G2 by A2, Def9
.= cod F by A1, Def9 ;
then G * F = RingMorphismStr(# G1,G3,(g * f) #) by A3, A4, Def10;
then A5: ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
G1 <= G3 by A1, A2, Th8;
hence G * F is Morphism of G1,G3 by A5, Def9; :: thesis: verum