let C1, C2 be non empty strict quasi-discrete AltCatStr ; ( the carrier of C1 = A & ( for i being object of C1 holds <^i,i^> = {(id i)} ) & the carrier of C2 = A & ( for i being object of C2 holds <^i,i^> = {(id i)} ) implies C1 = C2 )
assume that
A19:
the carrier of C1 = A
and
A20:
for i being object of C1 holds <^i,i^> = {(id i)}
and
A21:
the carrier of C2 = A
and
A22:
for i being object of C2 holds <^i,i^> = {(id i)}
; C1 = C2
A23:
now let i,
j,
k be
set ;
( i in A & j in A & k in A implies the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3) )assume that A24:
i in A
and A25:
(
j in A &
k in A )
;
the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)reconsider i2 =
i as
object of
C2 by A21, A24;
reconsider i1 =
i as
object of
C1 by A19, A24;
per cases
( ( i = j & j = k ) or i <> j or j <> k )
;
suppose A26:
(
i = j &
j = k )
;
the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)A27:
(
<^i2,i2^> = {(id i2)} & the
Comp of
C2 . (
i2,
i2,
i2) is
Function of
[:<^i2,i2^>,<^i2,i2^>:],
<^i2,i2^> )
by A22;
(
<^i1,i1^> = {(id i1)} & the
Comp of
C1 . (
i1,
i1,
i1) is
Function of
[:<^i1,i1^>,<^i1,i1^>:],
<^i1,i1^> )
by A20;
hence the
Comp of
C1 . (
i,
j,
k) =
(
(id i),
(id i))
:-> (id i)
by A26, FUNCOP_1:def 10
.=
the
Comp of
C2 . (
i,
j,
k)
by A26, A27, FUNCOP_1:def 10
;
verum end; suppose A28:
(
i <> j or
j <> k )
;
the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)reconsider j1 =
j,
k1 =
k as
object of
C1 by A19, A25;
A29:
(
<^i1,j1^> = {} or
<^j1,k1^> = {} )
by A28, Def20;
reconsider j2 =
j,
k2 =
k as
object of
C2 by A21, A25;
A30:
( the
Comp of
C2 . (
i2,
j2,
k2) is
Function of
[:<^j2,k2^>,<^i2,j2^>:],
<^i2,k2^> & the
Comp of
C1 . (
i1,
j1,
k1) is
Function of
[:<^j1,k1^>,<^i1,j1^>:],
<^i1,k1^> )
;
(
<^i2,j2^> = {} or
<^j2,k2^> = {} )
by A28, Def20;
hence
the
Comp of
C1 . (
i,
j,
k)
= the
Comp of
C2 . (
i,
j,
k)
by A29, A30;
verum end; end;
then
the Arrows of C1 = the Arrows of C2
by A19, A21, Th9;
hence
C1 = C2
by A19, A21, A23, Th10; verum