let V be Ring_DOMAIN; for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means dom $1 = cod $2;
let g, f be Element of Morphs V; ( dom g = cod f implies g * f in Morphs V )
assume
S1[g,f]
; g * f in Morphs V
then consider G1, G2, G3 being Element of V such that
A1:
( G1 <= G2 & G2 <= G3 )
and
A2:
g is Morphism of G2,G3
and
A3:
f is Morphism of G1,G2
by Th19;
reconsider f9 = f as Morphism of G1,G2 by A3;
reconsider g9 = g as Morphism of G2,G3 by A2;
( G1 <= G3 & g9 *' f9 = g9 * f9 )
by A1, Def10, Th5;
hence
g * f in Morphs V
by Def17; verum