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
A66:
the carrier of C1 = Funct (A,B)
and
A67:
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
A68:
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
A69:
the carrier of C2 = Funct (A,B)
and
A70:
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
A71:
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;
A72:
for i, j being object 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
object ;
( 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 A73:
i in the
carrier of
C1
and A74:
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 A69, A74, Def10;
reconsider f =
i as
strict covariant Functor of
A,
B by A66, A73, Def10;
hence
the
Arrows of
C1 . (
i,
j)
= the
Arrows of
C2 . (
i,
j)
by TARSKI:2;
verum
end;
then A75:
the Arrows of C1 = the Arrows of C2
by A66, A69, ALTCAT_1:6;
for i, j, k being object 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
object ;
( 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 A76:
i in the
carrier of
C1
and A77:
j in the
carrier of
C1
and A78:
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 A66, A78, Def10;
reconsider g =
j as
strict covariant Functor of
A,
B by A66, A77, Def10;
reconsider f =
i as
strict covariant Functor of
A,
B by A66, A76, 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 A79:
( 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,k)thus
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 A79;
suppose A80:
the
Arrows of
C1 . (
i,
j)
= {}
;
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)reconsider T = the
carrier of
C2 as non
empty set ;
reconsider i9 =
i,
j9 =
j,
k9 =
k as
Element of
T by A66, A69, A76, A77, A78;
the
Arrows of
C2 . (
i,
j)
= {}
by A66, A69, A72, A80, ALTCAT_1:6;
then A81:
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {}
by ZFMISC_1:90;
A82:
{| 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 4
;
A83:
{| 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 3
;
the
Comp of
C2 . [i9,j9,k9] = the
Comp of
C2 . (
i9,
j9,
k9)
by MULTOP_1:def 1;
then A84:
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 A82, A83, PBOOLE:def 15;
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 4
;
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 3
;
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 A66, A69, A75, A85, A86, PBOOLE:def 15;
hence
the
Comp of
C1 . (
i,
j,
k)
= the
Comp of
C2 . (
i,
j,
k)
by A81, A84;
verum end; suppose A87:
the
Arrows of
C1 . (
j,
k)
= {}
;
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)reconsider T = the
carrier of
C2 as non
empty set ;
reconsider i9 =
i,
j9 =
j,
k9 =
k as
Element of
T by A66, A69, A76, A77, A78;
the
Arrows of
C2 . (
j,
k)
= {}
by A66, A69, A72, A87, ALTCAT_1:6;
then A88:
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {}
by ZFMISC_1:90;
A89:
{| 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 4
;
A90:
{| 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 3
;
the
Comp of
C2 . [i9,j9,k9] = the
Comp of
C2 . (
i9,
j9,
k9)
by MULTOP_1:def 1;
then A91:
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 A89, A90, PBOOLE:def 15;
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 4
;
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 3
;
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 A66, A69, A75, A92, A93, PBOOLE:def 15;
hence
the
Comp of
C1 . (
i,
j,
k)
= the
Comp of
C2 . (
i,
j,
k)
by A88, A91;
verum end;
end; end; suppose that A94:
the
Arrows of
C1 . (
i,
j)
<> {}
and A95:
the
Arrows of
C1 . (
j,
k)
<> {}
;
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)reconsider T = the
carrier of
C2 as non
empty set ;
reconsider i9 =
i,
j9 =
j,
k9 =
k as
Element of
T by A66, A69, A76, A77, A78;
A96:
{| 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 4
;
A97:
{| 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 3
;
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 A96, A97, PBOOLE:def 15;
A98:
{| 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 4
;
A99:
{| 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 3
;
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 A66, A69, A75, A98, A99, PBOOLE:def 15;
A100:
the
Arrows of
C2 . (
j,
k)
<> {}
by A66, A69, A72, A95, ALTCAT_1:6;
A101:
the
Arrows of
C2 . (
i,
j)
<> {}
by A66, A69, A72, A94, ALTCAT_1:6;
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,b)let 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 A100;
then A102:
g is_naturally_transformable_to h
by A70;
reconsider a =
a as
natural_transformation of
g,
h by A70, A100;
b in the
Arrows of
C2 . (
i,
j)
by A101;
then A103:
f is_naturally_transformable_to g
by A70;
reconsider b =
b as
natural_transformation of
f,
g by A70, A101;
( 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 A68, A71, A102, A103;
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 A66, A69, A75, ALTCAT_1:8; verum