let f, g be strict GroupMorphism; :: thesis: ( dom g = cod f implies ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) ) )
assume A1: dom g = cod f ; :: thesis: ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# 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 Def12;
reconsider g9 = g as strict Morphism of cod f, cod g by A1, Def12;
consider f0 being Function of (dom f),(cod f) such that
A2: f9 = GroupMorphismStr(# (dom f),(cod f),f0 #) ;
consider g0 being Function of (cod f),(cod g) such that
A3: g9 = GroupMorphismStr(# (cod f),(cod g),g0 #) by Th13;
take dom f ; :: thesis: ex G2, G3 being AddGroup ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# (dom f),G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# (dom f),G3,(g0 * f0) #) )
take cod f ; :: thesis: ex G3 being AddGroup ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st
( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),G3,g0 #) & g * f = GroupMorphismStr(# (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 = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take f0 ; :: thesis: ex g0 being Function of (cod f),(cod g) st
( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take g0 ; :: thesis: ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
thus ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A2, A3, Th18; :: thesis: verum