set X = Morphs V;
defpred S₁[ Element of Morphs V, Element of Morphs V] means dom' $1 = cod' $2;
deffunc H₁( Element of Morphs V, Element of Morphs V) -> LModMorphismStr over R = $1 * $2;
A1: for g, f being Element of Morphs V st S₁[g,f] holds
H₁(g,f) in Morphs V by Th9;
consider c being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) such that
A2: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff S₁[g,f] ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = H₁(g,f) ) ) from BINOP_1:sch 8(A1);
take c ; :: thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) )
thus ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) ) by A2; :: thesis: verum