let R be Ring; :: thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
g * f in Morphs V
let V be LeftMod_DOMAIN of R; :: 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 strict Element of V such that
A1: g is Morphism of G2,G3 and
A2: f is Morphism of G1,G2 by Th8;
reconsider f9 = f as Morphism of G1,G2 by A2;
reconsider g9 = g as Morphism of G2,G3 by A1;
g9 * f9 = g9 *' f9 ;
hence g * f in Morphs V by Def7; :: thesis: verum