let C1, C2 be non empty strict pseudo-functional AltCatStr ; ( the carrier of C1 = A & ( for a1, a2 being object of C1 holds <^a1,a2^> = Funcs a1,a2 ) & the carrier of C2 = A & ( for a1, a2 being object of C2 holds <^a1,a2^> = Funcs a1,a2 ) implies C1 = C2 )
assume that
A18:
the carrier of C1 = A
and
A19:
for a1, a2 being object of C1 holds <^a1,a2^> = Funcs a1,a2
and
A20:
the carrier of C2 = A
and
A21:
for a1, a2 being object of C2 holds <^a1,a2^> = Funcs a1,a2
; C1 = C2
A22:
now let i,
j be
set ;
( i in A & j in A implies the Arrows of C1 . i,j = the Arrows of C2 . i,j )assume A23:
(
i in A &
j in A )
;
the Arrows of C1 . i,j = the Arrows of C2 . i,jthen reconsider a1 =
i,
a2 =
j as
object of
C1 by A18;
reconsider b1 =
i,
b2 =
j as
object of
C2 by A20, A23;
thus the
Arrows of
C1 . i,
j =
<^a1,a2^>
.=
Funcs a1,
a2
by A19
.=
<^b1,b2^>
by A21
.=
the
Arrows of
C2 . i,
j
;
verum end;
A24:
now let i,
j,
k be
set ;
( i in A & j in A & k in A implies the Comp of C1 . i,j,k = the Comp of C2 . i,j,k )assume A25:
(
i in A &
j in A &
k in A )
;
the Comp of C1 . i,j,k = the Comp of C2 . i,j,kthen reconsider a1 =
i,
a2 =
j,
a3 =
k as
object of
C1 by A18;
reconsider b1 =
i,
b2 =
j,
b3 =
k as
object of
C2 by A20, A25;
(
<^a2,a3^> = <^b2,b3^> &
<^a1,a2^> = <^b1,b2^> )
by A18, A22;
hence the
Comp of
C1 . i,
j,
k =
(FuncComp (Funcs b1,b2),(Funcs b2,b3)) | [:<^b2,b3^>,<^b1,b2^>:]
by Def15
.=
the
Comp of
C2 . i,
j,
k
by Def15
;
verum end;
the Arrows of C1 = the Arrows of C2
by A18, A20, A22, Th8;
hence
C1 = C2
by A18, A20, A24, Th10; verum