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; ( ( 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) #)
; 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
; verum