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 g9 = g as Morphism of cod f, cod g by A1, Th3;
consider g0 being Function of (cod f),(cod g) such that
A2: g9 = RingMorphismStr(# (cod f),(cod g),g0 #) by A1;
reconsider f9 = f as Morphism of dom f, cod f by Th3;
consider f0 being Function of (dom f),(cod f) such that
A3: f9 = RingMorphismStr(# (dom f),(cod f),f0 #) ;
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, A3, A2, Def9; :: thesis: verum