set X = Morphs V;
defpred S1[ 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); ( ( 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 S1[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 S1[g,f] )
and
A6:
for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f
; c1 = c2
set V9 = dom c1;
A7:
dom c1 c= [:(Morphs V),(Morphs V):]
by RELAT_1:def 18;
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 ;
( [x,y] in dom c1 implies c1 . (x,y) = c2 . (x,y) )
assume A12:
[x,y] in dom c1
;
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;
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; verum