let f, g be strict RingMorphism; :: thesis: ( dom g = cod f implies ex G1, G2, G3 being Ring ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = RingMorphismStr(# G1,G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) ) )
assume A1: dom g = cod f ; :: thesis: ex G1, G2, G3 being Ring ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = RingMorphismStr(# G1,G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )
set G1 = dom f;
set G2 = cod f;
set G3 = cod g;
reconsider f' = f as Morphism of dom f, cod f by Th6;
reconsider g' = g as Morphism of cod f, cod g by A1, Th6;
consider f0 being Function of (dom f),(cod f) such that
A2: f' = RingMorphismStr(# (dom f),(cod f),f0 #) ;
consider g0 being Function of (cod f),(cod g) such that
A3: g' = RingMorphismStr(# (cod f),(cod g),g0 #) by A1;
take dom f ; :: thesis: ex G2, G3 being Ring ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st
( f = RingMorphismStr(# (dom f),G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# (dom f),G3,(g0 * f0) #) )
take cod f ; :: thesis: ex G3 being Ring ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st
( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),G3,g0 #) & g * f = RingMorphismStr(# (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 = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take f0 ; :: thesis: ex g0 being Function of (cod f),(cod g) st
( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take g0 ; :: thesis: ( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
thus ( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A1, A2, A3, Def10; :: thesis: verum