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

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