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