consider G1', G2'' being Ring such that
G1' <= G2'' and
A9: dom F = G1' and
A10: cod F = G2'' and
A11: 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 A11;
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
A12: 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
A13: 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
A14: G2' <= G3' and
A15: dom G = G2' and
cod G = G3' and
A16: RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) is Morphism of G2',G3' by Lm6;
reconsider F' = F' as Morphism of G1',G2' by A1, A15, A10;
consider f' being Function of G1',G2' such that
A17: F' = RingMorphismStr(# G1',G2',f' #) by A1, A15, A9;
reconsider G' = RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) as Morphism of G2',G3' by A16;
consider g' being Function of G2',G3' such that
A18: G' = RingMorphismStr(# G2',G3',g' #) by A14, Lm8;
thus S1 = RingMorphismStr(# G1',G3',(g' * f') #) by A12, A18, A17
.= S2 by A13, A18, A17 ; :: thesis: verum