let C1, C2 be non empty transitive strict AltCatStr ; ( the carrier of C1 = Funct A,B & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C1 . F,G iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C1 . F,G,H & f . t2,t1 = t2 `*` t1 ) ) & the carrier of C2 = Funct A,B & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C2 . F,G iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C2 . F,G,H & f . t2,t1 = t2 `*` t1 ) ) implies C1 = C2 )
assume that
A62:
the carrier of C1 = Funct A,B
and
A63:
for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C1 . F,G iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) )
and
A64:
for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C1 . F,G,H & f . t2,t1 = t2 `*` t1 )
and
A65:
the carrier of C2 = Funct A,B
and
A66:
for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C2 . F,G iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) )
and
A67:
for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C2 . F,G,H & f . t2,t1 = t2 `*` t1 )
; C1 = C2
set R = the carrier of C1;
set T = the carrier of C2;
set N = the Arrows of C1;
set M = the Arrows of C2;
set O = the Comp of C1;
set P = the Comp of C2;
A68:
for i, j being set st i in the carrier of C1 & j in the carrier of C2 holds
the Arrows of C1 . i,j = the Arrows of C2 . i,j
proof
let i,
j be
set ;
( i in the carrier of C1 & j in the carrier of C2 implies the Arrows of C1 . i,j = the Arrows of C2 . i,j )
assume that A69:
i in the
carrier of
C1
and A70:
j in the
carrier of
C2
;
the Arrows of C1 . i,j = the Arrows of C2 . i,j
reconsider g =
j as
strict covariant Functor of
A,
B by A65, A70, Def10;
reconsider f =
i as
strict covariant Functor of
A,
B by A62, A69, Def10;
hence
the
Arrows of
C1 . i,
j = the
Arrows of
C2 . i,
j
by TARSKI:2;
verum
end;
then A71:
the Arrows of C1 = the Arrows of C2
by A62, A65, ALTCAT_1:8;
for i, j, k being set st i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 holds
the Comp of C1 . i,j,k = the Comp of C2 . i,j,k
proof
let i,
j,
k be
set ;
( i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 implies the Comp of C1 . i,j,k = the Comp of C2 . i,j,k )
assume that A72:
i in the
carrier of
C1
and A73:
j in the
carrier of
C1
and A74:
k in the
carrier of
C1
;
the Comp of C1 . i,j,k = the Comp of C2 . i,j,k
reconsider h =
k as
strict covariant Functor of
A,
B by A62, A74, Def10;
reconsider g =
j as
strict covariant Functor of
A,
B by A62, A73, Def10;
reconsider f =
i as
strict covariant Functor of
A,
B by A62, A72, Def10;
per cases
( the Arrows of C1 . i,j = {} or the Arrows of C1 . j,k = {} or ( the Arrows of C1 . i,j <> {} & the Arrows of C1 . j,k <> {} ) )
;
suppose A75:
( the
Arrows of
C1 . i,
j = {} or the
Arrows of
C1 . j,
k = {} )
;
the Comp of C1 . i,j,k = the Comp of C2 . i,j,kthus
the
Comp of
C1 . i,
j,
k = the
Comp of
C2 . i,
j,
k
verumproof
per cases
( the Arrows of C1 . i,j = {} or the Arrows of C1 . j,k = {} )
by A75;
suppose A76:
the
Arrows of
C1 . i,
j = {}
;
the Comp of C1 . i,j,k = the Comp of C2 . i,j,kreconsider T = the
carrier of
C2 as non
empty set ;
reconsider i9 =
i,
j9 =
j,
k9 =
k as
Element of
T by A62, A65, A72, A73, A74;
the
Arrows of
C2 . i,
j = {}
by A62, A65, A68, A76, ALTCAT_1:8;
then A77:
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):] = {}
by ZFMISC_1:113;
A78:
{|the Arrows of C2,the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2,the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):]
by ALTCAT_1:def 6
;
A79:
{|the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
the
Arrows of
C2 . i9,
k9
by ALTCAT_1:def 5
;
the
Comp of
C2 . [i9,j9,k9] = the
Comp of
C2 . i9,
j9,
k9
by MULTOP_1:def 1;
then A80:
the
Comp of
C2 . i9,
j9,
k9 is
Function of
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):],
(the Arrows of C2 . i9,k9)
by A78, A79, PBOOLE:def 18;
A81:
{|the Arrows of C2,the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2,the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):]
by ALTCAT_1:def 6
;
A82:
{|the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
the
Arrows of
C2 . i9,
k9
by ALTCAT_1:def 5
;
the
Comp of
C1 . [i9,j9,k9] = the
Comp of
C1 . i9,
j9,
k9
by MULTOP_1:def 1;
then
the
Comp of
C1 . i9,
j9,
k9 is
Function of
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):],
(the Arrows of C2 . i9,k9)
by A62, A65, A71, A81, A82, PBOOLE:def 18;
hence
the
Comp of
C1 . i,
j,
k = the
Comp of
C2 . i,
j,
k
by A77, A80;
verum end; suppose A83:
the
Arrows of
C1 . j,
k = {}
;
the Comp of C1 . i,j,k = the Comp of C2 . i,j,kreconsider T = the
carrier of
C2 as non
empty set ;
reconsider i9 =
i,
j9 =
j,
k9 =
k as
Element of
T by A62, A65, A72, A73, A74;
the
Arrows of
C2 . j,
k = {}
by A62, A65, A68, A83, ALTCAT_1:8;
then A84:
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):] = {}
by ZFMISC_1:113;
A85:
{|the Arrows of C2,the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2,the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):]
by ALTCAT_1:def 6
;
A86:
{|the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
the
Arrows of
C2 . i9,
k9
by ALTCAT_1:def 5
;
the
Comp of
C2 . [i9,j9,k9] = the
Comp of
C2 . i9,
j9,
k9
by MULTOP_1:def 1;
then A87:
the
Comp of
C2 . i9,
j9,
k9 is
Function of
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):],
(the Arrows of C2 . i9,k9)
by A85, A86, PBOOLE:def 18;
A88:
{|the Arrows of C2,the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2,the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):]
by ALTCAT_1:def 6
;
A89:
{|the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
the
Arrows of
C2 . i9,
k9
by ALTCAT_1:def 5
;
the
Comp of
C1 . [i9,j9,k9] = the
Comp of
C1 . i9,
j9,
k9
by MULTOP_1:def 1;
then
the
Comp of
C1 . i9,
j9,
k9 is
Function of
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):],
(the Arrows of C2 . i9,k9)
by A62, A65, A71, A88, A89, PBOOLE:def 18;
hence
the
Comp of
C1 . i,
j,
k = the
Comp of
C2 . i,
j,
k
by A84, A87;
verum end;
end; end; suppose that A90:
the
Arrows of
C1 . i,
j <> {}
and A91:
the
Arrows of
C1 . j,
k <> {}
;
the Comp of C1 . i,j,k = the Comp of C2 . i,j,kreconsider T = the
carrier of
C2 as non
empty set ;
reconsider i9 =
i,
j9 =
j,
k9 =
k as
Element of
T by A62, A65, A72, A73, A74;
A92:
{|the Arrows of C2,the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2,the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):]
by ALTCAT_1:def 6
;
A93:
{|the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
the
Arrows of
C2 . i9,
k9
by ALTCAT_1:def 5
;
the
Comp of
C2 . [i9,j9,k9] = the
Comp of
C2 . i9,
j9,
k9
by MULTOP_1:def 1;
then reconsider t2 = the
Comp of
C2 . i,
j,
k as
Function of
[:(the Arrows of C2 . j,k),(the Arrows of C2 . i,j):],
(the Arrows of C2 . i,k) by A92, A93, PBOOLE:def 18;
A94:
{|the Arrows of C2,the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2,the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
[:(the Arrows of C2 . j9,k9),(the Arrows of C2 . i9,j9):]
by ALTCAT_1:def 6
;
A95:
{|the Arrows of C2|} . [i9,j9,k9] =
{|the Arrows of C2|} . i9,
j9,
k9
by MULTOP_1:def 1
.=
the
Arrows of
C2 . i9,
k9
by ALTCAT_1:def 5
;
the
Comp of
C1 . [i9,j9,k9] = the
Comp of
C1 . i9,
j9,
k9
by MULTOP_1:def 1;
then reconsider t1 = the
Comp of
C1 . i,
j,
k as
Function of
[:(the Arrows of C2 . j,k),(the Arrows of C2 . i,j):],
(the Arrows of C2 . i,k) by A62, A65, A71, A94, A95, PBOOLE:def 18;
A96:
the
Arrows of
C2 . j,
k <> {}
by A62, A65, A68, A91, ALTCAT_1:8;
A97:
the
Arrows of
C2 . i,
j <> {}
by A62, A65, A68, A90, ALTCAT_1:8;
for
a being
Element of the
Arrows of
C2 . j,
k for
b being
Element of the
Arrows of
C2 . i,
j holds
t1 . a,
b = t2 . a,
b
proof
let a be
Element of the
Arrows of
C2 . j,
k;
for b being Element of the Arrows of C2 . i,j holds t1 . a,b = t2 . a,blet b be
Element of the
Arrows of
C2 . i,
j;
t1 . a,b = t2 . a,b
a in the
Arrows of
C2 . j,
k
by A96;
then A98:
g is_naturally_transformable_to h
by A66;
reconsider a =
a as
natural_transformation of
g,
h by A66, A96;
b in the
Arrows of
C2 . i,
j
by A97;
then A99:
f is_naturally_transformable_to g
by A66;
reconsider b =
b as
natural_transformation of
f,
g by A66, A97;
( ex
t19 being
Function st
(
t19 = the
Comp of
C1 . f,
g,
h &
t19 . a,
b = a `*` b ) & ex
t29 being
Function st
(
t29 = the
Comp of
C2 . f,
g,
h &
t29 . a,
b = a `*` b ) )
by A64, A67, A98, A99;
hence
t1 . a,
b = t2 . a,
b
;
verum
end; hence
the
Comp of
C1 . i,
j,
k = the
Comp of
C2 . i,
j,
k
by BINOP_1:2;
verum end;
end;
hence
C1 = C2
by A62, A65, A71, ALTCAT_1:10; verum