let f, g be strict RingMorphism; ( 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
; 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
; 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
; 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
; 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
; 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
; ( 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; verum