let V be Ring_DOMAIN; :: thesis: for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
set X = Morphs V;
defpred S₁[ Element of Morphs V, Element of Morphs V] means dom $1 = cod $2;
let g, f be Element of Morphs V; :: thesis: ( dom g = cod f implies g * f in Morphs V )
assume S₁[g,f] ; :: thesis: g * f in Morphs V
then consider G1, G2, G3 being Element of V such that
A1: ( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by Th24;
A2: G1 <= G3 by A1, Th8;
reconsider g' = g as Morphism of G2,G3 by A1;
reconsider f' = f as Morphism of G1,G2 by A1;
g' *' f' = g' * f' by A1, Def11;
hence g * f in Morphs V by A2, Def18; :: thesis: verum