let R be Ring; :: thesis: for G2, G3, G1 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 G2, G3, G1 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 linear by Th14;
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 linear by Th14;
dom G = G2 by Def11
.= cod F by Def11 ;
then G * F = LModMorphismStr(# G1,G3,(g * f) #) by A1, A2, Def13;
then ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
hence G * F is strict Morphism of G1,G3 by Def11; :: thesis: verum