let o1, o2 be BinComp of (the_hom_sets_of C); ( ( for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) implies o1 = o2 )
assume that
A15:
for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
and
A16:
for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
; o1 = o2
now for a being object st a in [: the carrier of C, the carrier of C, the carrier of C:] holds
o1 . a = o2 . alet a be
object ;
( a in [: the carrier of C, the carrier of C, the carrier of C:] implies o1 . a = o2 . a )assume
a in [: the carrier of C, the carrier of C, the carrier of C:]
;
o1 . a = o2 . athen consider i,
j,
k being
Object of
C such that A17:
a = [i,j,k]
by DOMAIN_1:3;
thus o1 . a =
o1 . (
i,
j,
k)
by A17, MULTOP_1:def 1
.=
the
Comp of
C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]
by A15
.=
o2 . (
i,
j,
k)
by A16
.=
o2 . a
by A17, MULTOP_1:def 1
;
verum end;
hence
o1 = o2
; verum