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
A14:
the carrier of C1 = A
and
A15:
for a1, a2 being Object of C1 holds <^a1,a2^> = Funcs (a1,a2)
and
A16:
the carrier of C2 = A
and
A17:
for a1, a2 being Object of C2 holds <^a1,a2^> = Funcs (a1,a2)
; C1 = C2
A18:
now for i, j being object st i in A & j in A holds
the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)let i,
j be
object ;
( i in A & j in A implies the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) )assume A19:
(
i in A &
j in A )
;
the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)then reconsider a1 =
i,
a2 =
j as
Object of
C1 by A14;
reconsider b1 =
i,
b2 =
j as
Object of
C2 by A16, A19;
thus the
Arrows of
C1 . (
i,
j) =
<^a1,a2^>
.=
Funcs (
a1,
a2)
by A15
.=
<^b1,b2^>
by A17
.=
the
Arrows of
C2 . (
i,
j)
;
verum end;
A20:
now for i, j, k being object st i in A & j in A & k in A holds
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)let i,
j,
k be
object ;
( 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 A21:
(
i in A &
j in A &
k in A )
;
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)then reconsider a1 =
i,
a2 =
j,
a3 =
k as
Object of
C1 by A14;
reconsider b1 =
i,
b2 =
j,
b3 =
k as
Object of
C2 by A16, A21;
(
<^a2,a3^> = <^b2,b3^> &
<^a1,a2^> = <^b1,b2^> )
by A14, A18;
hence the
Comp of
C1 . (
i,
j,
k) =
(FuncComp ((Funcs (b1,b2)),(Funcs (b2,b3)))) | [:<^b2,b3^>,<^b1,b2^>:]
by Def13
.=
the
Comp of
C2 . (
i,
j,
k)
by Def13
;
verum end;
the Arrows of C1 = the Arrows of C2
by A14, A16, A18, Th2;
hence
C1 = C2
by A14, A16, A20, Th4; verum