set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means dom $1 = cod $2;
deffunc H1( Element of Morphs V, Element of Morphs V) -> strict RingMorphism = $1 * $2;
A1:
for g, f being Element of Morphs V st S1[g,f] holds
H1(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 S1[g,f] ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = H1(g,f) ) )
from BINOP_1:sch 8(A1);
take
c
; ( ( 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; verum