let R be Ring; :: thesis: for G1, G2, G3 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
let G1, G2, G3 be LeftMod of R; :: thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
let G be Morphism of G2,G3; :: thesis: for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
let F be Morphism of G1,G2; :: thesis: G * F is strict Morphism of G1,G3
consider g being Function of G2,G3 such that
A1: LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) and
( g is additive & g is homogeneous ) by Th7;
consider f being Function of G1,G2 such that
A2: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) and
( f is additive & f is homogeneous ) by Th7;
dom G = G2 by Def8
.= cod F by Def8 ;
then G * F = LModMorphismStr(# G1,G3,(g * f) #) by A1, A2, Def10;
then ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
hence G * F is strict Morphism of G1,G3 by Def8; :: thesis: verum