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