let G1, G2, G3 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, Def8
.= cod F by A1, Def8 ;
then G * F = RingMorphismStr(# G1,G3,(g * f) #) by A3, A4, Def9;
then A5: ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
G1 <= G3 by A1, A2, Th5;
hence G * F is Morphism of G1,G3 by A5, Def8; :: thesis: verum