let S1, S2 be strict RingMorphism; :: thesis: ( ( for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S1 = RingMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S2 = RingMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A9: for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S1 = RingMorphismStr(# G1,G3,(g * f) #) and
A10: for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S2 = RingMorphismStr(# G1,G3,(g * f) #) ; :: thesis: S1 = S2
consider G2', G3' being Ring such that
A11: G2' <= G3' and
A12: ( dom G = G2' & cod G = G3' ) and
A13: RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) is Morphism of G2',G3' by Lm6;
reconsider G' = RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) as Morphism of G2',G3' by A13;
consider G1', G2'' being Ring such that
G1' <= G2'' and
A14: ( dom F = G1' & cod F = G2'' ) and
A15: RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) is Morphism of G1',G2'' by Lm6;
reconsider F' = RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) as Morphism of G1',G2'' by A15;
reconsider F' = F' as Morphism of G1',G2' by A1, A12, A14;
consider g' being Function of G2',G3' such that
A16: G' = RingMorphismStr(# G2',G3',g' #) by A11, Lm8;
consider f' being Function of G1',G2' such that
A17: F' = RingMorphismStr(# G1',G2',f' #) by A1, A12, A14;
thus S1 = RingMorphismStr(# G1',G3',(g' * f') #) by A9, A16, A17
.= S2 by A10, A16, A17 ; :: thesis: verum