let R be Ring; :: thesis: for f, g being strict LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) )
let f, g be strict LModMorphism of R; :: thesis: ( dom g = cod f implies ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) ) )
assume A1: dom g = cod f ; :: thesis: ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) )
set G1 = dom f;
set G2 = cod f;
set G3 = cod g;
reconsider f9 = f as strict Morphism of dom f, cod f by Def8;
reconsider g9 = g as strict Morphism of cod f, cod g by A1, Def8;
consider f0 being Function of (dom f),(cod f) such that
A2: f9 = LModMorphismStr(# (dom f),(cod f),f0 #) ;
consider g0 being Function of (cod f),(cod g) such that
A3: g9 = LModMorphismStr(# (cod f),(cod g),g0 #) by Th8;
take dom f ; :: thesis: ex G2, G3 being LeftMod of R ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# (dom f),G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# (dom f),G3,(g0 * f0) #) )
take cod f ; :: thesis: ex G3 being LeftMod of R ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st
( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),G3,g0 #) & g * f = LModMorphismStr(# (dom f),G3,(g0 * f0) #) )
take cod g ; :: thesis: ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),(cod g) st
( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take f0 ; :: thesis: ex g0 being Function of (cod f),(cod g) st
( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take g0 ; :: thesis: ( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
thus ( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A2, A3, Th13; :: thesis: verum