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:1;
verum
end;
then A71:
the Arrows of C1 = the Arrows of C2
by A62, A65, ALTCAT_1:6;
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,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 A75;
suppose A76:
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 A62, A65, A72, A73, A74;
the
Arrows of
C2 . (
i,
j)
= {}
by A62, A65, A68, A76, ALTCAT_1:6;
then A77:
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {}
by ZFMISC_1:90;
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 4
;
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 3
;
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 15;
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 4
;
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 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 A62, A65, A71, A81, A82, PBOOLE:def 15;
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,k)reconsider 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:6;
then A84:
[:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {}
by ZFMISC_1:90;
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
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 15;
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 4
;
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 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 A62, A65, A71, A88, A89, PBOOLE:def 15;
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,k)reconsider 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 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
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 15;
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 4
;
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 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 A62, A65, A71, A94, A95, PBOOLE:def 15;
A96:
the
Arrows of
C2 . (
j,
k)
<> {}
by A62, A65, A68, A91, ALTCAT_1:6;
A97:
the
Arrows of
C2 . (
i,
j)
<> {}
by A62, A65, A68, A90, 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 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:8; verum