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) -> strict RingMorphism = $1 * $2;
A1: for g, f being Element of Morphs V st S₁[g,f] holds
H₁(g,f) in Morphs V by Th20;
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