set X = Morphs V;
defpred S₁[ Element of Morphs V, Element of Morphs V] means dom $1 = cod $2;
let c1, c2 be PartFunc of [:(Morphs V),(Morphs V):],(Morphs V); :: thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ) implies c1 = c2 )
assume that
A3: for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff S₁[g,f] ) and
A4: for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f and
A5: for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff S₁[g,f] ) and
A6: for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ; :: thesis: c1 = c2
set V9 = dom c1;
A7: dom c1 c= [:(Morphs V),(Morphs V):] by RELAT_1:def 18;

now :: thesis: for x being object st x in dom c1 holds
x in dom c2

let x be object ; :: thesis: ( x in dom c1 implies x in dom c2 )
assume A8: x in dom c1 ; :: thesis: x in dom c2
then consider g, f being Element of Morphs V such that
A9: x = [g,f] by A7, SUBSET_1:43;
S₁[g,f] by A3, A8, A9;
hence x in dom c2 by A5, A9; :: thesis: verum

end;

then A10: dom c1 c= dom c2 by TARSKI:def 3;
A11: for x, y being object st [x,y] in dom c1 holds
c1 . (x,y) = c2 . (x,y)

proof

let x, y be object ; :: thesis: ( [x,y] in dom c1 implies c1 . (x,y) = c2 . (x,y) )
assume A12: [x,y] in dom c1 ; :: thesis: c1 . (x,y) = c2 . (x,y)
then reconsider x = x, y = y as Element of Morphs V by A7, ZFMISC_1:87;
c1 . (x,y) = x * y by A4, A12;
hence c1 . (x,y) = c2 . (x,y) by A6, A10, A12; :: thesis: verum

end;

now :: thesis: for x being object st x in dom c2 holds
x in dom c1

let x be object ; :: thesis: ( x in dom c2 implies x in dom c1 )
assume A13: x in dom c2 ; :: thesis: x in dom c1
dom c2 c= [:(Morphs V),(Morphs V):] by RELAT_1:def 18;
then consider g, f being Element of Morphs V such that
A14: x = [g,f] by A13, SUBSET_1:43;
S₁[g,f] by A5, A13, A14;
hence x in dom c1 by A3, A14; :: thesis: verum

end;

then dom c2 c= dom c1 by TARSKI:def 3;
then dom c1 = dom c2 by A10, XBOOLE_0:def 10;
hence c1 = c2 by A11, BINOP_1:20; :: thesis: verum