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