let C1, C2 be non empty transitive AltCatStr ; :: thesis: ( the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) implies AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #) )
assume that
A1:
the carrier of C1 = F1()
and
A2:
for a, b being object of C1 holds <^a,b^> = F2(a,b)
and
A3:
for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g)
and
A4:
the carrier of C2 = F1()
and
A5:
for a, b being object of C2 holds <^a,b^> = F2(a,b)
and
A6:
for a, b, c being object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g)
; :: thesis: AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
A7:
now let i be
set ;
:: thesis: ( i in [:F1(),F1():] implies the Arrows of C1 . i = the Arrows of C2 . i )assume
i in [:F1(),F1():]
;
:: thesis: the Arrows of C1 . i = the Arrows of C2 . ithen consider a,
b being
set such that A8:
(
a in F1() &
b in F1() &
i = [a,b] )
by ZFMISC_1:def 2;
reconsider a1 =
a,
b1 =
b as
object of
C1 by A1, A8;
reconsider a2 =
a,
b2 =
b as
object of
C2 by A4, A8;
thus the
Arrows of
C1 . i =
<^a1,b1^>
by A8
.=
F2(
a1,
b1)
by A2
.=
<^a2,b2^>
by A5
.=
the
Arrows of
C2 . i
by A8
;
:: thesis: verum end;
then A9:
the Arrows of C1 = the Arrows of C2
by A1, A4, PBOOLE:3;
now let i be
set ;
:: thesis: ( i in [:F1(),F1(),F1():] implies the Comp of C1 . i = the Comp of C2 . i )assume
i in [:F1(),F1(),F1():]
;
:: thesis: the Comp of C1 . i = the Comp of C2 . ithen consider a,
b,
c being
set such that A10:
(
a in F1() &
b in F1() &
c in F1() &
i = [a,b,c] )
by MCART_1:72;
reconsider a1 =
a,
b1 =
b,
c1 =
c as
object of
C1 by A1, A10;
reconsider a2 =
a,
b2 =
b,
c2 =
c as
object of
C2 by A4, A10;
A11:
( the
Comp of
C1 . i = the
Comp of
C1 . a1,
b1,
c1 & the
Comp of
C2 . i = the
Comp of
C2 . a2,
b2,
c2 )
by A10, MULTOP_1:def 1;
then A12:
(
dom (the Comp of C1 . a1,b1,c1) = [:<^b1,c1^>,<^a1,b1^>:] &
dom (the Comp of C2 . a2,b2,c2) = [:<^b1,c1^>,<^a1,b1^>:] )
by A9, FUNCT_2:def 1;
now let j be
set ;
:: thesis: ( j in [:<^b1,c1^>,<^a1,b1^>:] implies (the Comp of C1 . a1,b1,c1) . j = (the Comp of C2 . a2,b2,c2) . j )assume
j in [:<^b1,c1^>,<^a1,b1^>:]
;
:: thesis: (the Comp of C1 . a1,b1,c1) . j = (the Comp of C2 . a2,b2,c2) . jthen consider j1,
j2 being
set such that A13:
(
j1 in <^b1,c1^> &
j2 in <^a1,b1^> )
and A14:
j = [j1,j2]
by ZFMISC_1:def 2;
reconsider j1 =
j1 as
Morphism of
b1,
c1 by A13;
reconsider j2 =
j2 as
Morphism of
a1,
b1 by A13;
reconsider f1 =
j1 as
Morphism of
b2,
c2 by A1, A4, A7, PBOOLE:3;
reconsider f2 =
j2 as
Morphism of
a2,
b2 by A1, A4, A7, PBOOLE:3;
thus (the Comp of C1 . a1,b1,c1) . j =
(the Comp of C1 . a1,b1,c1) . j1,
j2
by A14
.=
j1 * j2
by A13, ALTCAT_1:def 10
.=
F3(
a1,
b1,
c1,
j2,
j1)
by A3, A13
.=
f1 * f2
by A6, A9, A13
.=
(the Comp of C2 . a2,b2,c2) . f1,
f2
by A9, A13, ALTCAT_1:def 10
.=
(the Comp of C2 . a2,b2,c2) . j
by A14
;
:: thesis: verum end; hence
the
Comp of
C1 . i = the
Comp of
C2 . i
by A11, A12, FUNCT_1:9;
:: thesis: verum end;
hence
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
by A1, A4, A9, PBOOLE:3; :: thesis: verum