:: INDEX_1 semantic presentation

registration

let A be non empty set ;
cluster V3 ManySortedSet of A;
existence

proof end;

end;

registration

let A be non empty set ;
cluster V2 -> V3 ManySortedSet of A;
coherence

proof end;

end;

definition

let C be Categorial Category;
let f be Morphism of C;
:: original: `2
redefine func f `2 -> Functor of f `11 ,f `12 ;
coherence

proof end;

end;

theorem :: INDEX_1:1

for C being Categorial Category
for f, g being Morphism of C st dom g = cod f holds
g * f = [[(dom f),(cod g)],((g `2 ) * (f `2 ))]

proof end;

theorem Th2: :: INDEX_1:2

for C being Category
for D, E being Categorial Category
for F being Functor of C,D
for G being Functor of C,E st F = G holds
Obj F = Obj G

proof end;

definition

let IT be Function;
attr IT is Category-yielding means :Def1: :: INDEX_1:def 1
for x being set st x in dom IT holds
IT . x is Category;

end;

:: deftheorem Def1 defines Category-yielding INDEX_1:def 1 :

registration

cluster Category-yielding set ;
existence

proof end;

end;

registration

let X be set ;
cluster Category-yielding ManySortedSet of X;
existence

proof end;

end;

definition

let A be set ;
mode ManySortedCategory of A is Category-yielding ManySortedSet of A;

end;

definition

let C be Category;
mode ManySortedSet of C is ManySortedSet of the Objects of C;
mode ManySortedCategory of C is ManySortedCategory of the Objects of C;

end;

registration

let X be set ;
let x be Category;
cluster X --> x -> Category-yielding ;
coherence

proof end;

end;

registration

let X be non empty set ;
cluster -> non empty ManySortedSet of X;
coherence

proof end;

end;

registration

let f be Category-yielding Function;
cluster rng f -> categorial ;
coherence

proof end;

end;

definition

let X be non empty set ;
let f be ManySortedCategory of X;
let x be Element of X;
:: original: .
redefine func f . x -> Category;
coherence

proof end;

end;

registration

let f be Function;
let g be Category-yielding Function;
cluster f * g -> Category-yielding ;
coherence

proof end;

end;

definition

let F be Category-yielding Function;
func Objs F -> non-empty Function means :Def2: :: INDEX_1:def 2
( dom it = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
it . x = the Objects of C ) );
existence

proof end;

uniqueness

proof end;

func Mphs F -> non-empty Function means :Def3: :: INDEX_1:def 3
( dom it = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
it . x = the Morphisms of C ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Objs INDEX_1:def 2 :

:: deftheorem Def3 defines Mphs INDEX_1:def 3 :

definition

let A be non empty set ;
let F be ManySortedCategory of A;
:: original: Objs
redefine func Objs F -> V2 ManySortedSet of A;
coherence

proof end;

:: original: Mphs
redefine func Mphs F -> V2 ManySortedSet of A;
coherence

proof end;

end;

theorem :: INDEX_1:3

for X being set
for C being Category holds
( Objs (X --> C) = X --> the Objects of C & Mphs (X --> C) = X --> the Morphisms of C )

proof end;

definition

let A, B be set ;
mode ManySortedSet of A,B -> set means :Def4: :: INDEX_1:def 4
ex f being ManySortedSet of A ex g being ManySortedSet of B st it = [f,g];
existence

proof end;

end;

:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :

definition

let A, B be set ;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
:: original: [
redefine func [f,g] -> ManySortedSet of A,B;
coherence

proof end;

end;

definition

let A, B be set ;
let X be ManySortedSet of A,B;
:: original: `1
redefine func X `1 -> ManySortedSet of A;
coherence

proof end;

:: original: `2
redefine func X `2 -> ManySortedSet of B;
coherence

proof end;

end;

definition

let A, B be set ;
let IT be ManySortedSet of A,B;
attr IT is Category-yielding_on_first means :Def5: :: INDEX_1:def 5
IT `1 is Category-yielding;
attr IT is Function-yielding_on_second means :Def6: :: INDEX_1:def 6
IT `2 is Function-yielding;

end;

:: deftheorem Def5 defines Category-yielding_on_first INDEX_1:def 5 :

:: deftheorem Def6 defines Function-yielding_on_second INDEX_1:def 6 :

registration

let A, B be set ;
cluster Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;
existence

proof end;

end;

definition

let A, B be set ;
let X be Category-yielding_on_first ManySortedSet of A,B;
:: original: `1
redefine func X `1 -> ManySortedCategory of A;
coherence by Def5;

end;

definition

let A, B be set ;
let X be Function-yielding_on_second ManySortedSet of A,B;
:: original: `2
redefine func X `2 -> ManySortedFunction of B;
coherence by Def6;

end;

registration

let f be Function-yielding Function;
cluster rng f -> functional ;
coherence

proof end;

end;

definition

let A, B be set ;
let f be ManySortedCategory of A;
let g be ManySortedFunction of B;
:: original: [
redefine func [f,g] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;
coherence

proof end;

end;

definition

let A be non empty set ;
let F, G be ManySortedCategory of A;
mode ManySortedFunctor of F,G -> ManySortedFunction of A means :Def7: :: INDEX_1:def 7
for a being Element of A holds it . a is Functor of F . a,G . a;
existence

proof end;

end;

:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :

scheme :: INDEX_1:sch 1
LambdaMSFr{ F₁() -> non empty set , F₂() -> ManySortedCategory of F₁(), F₃() -> ManySortedCategory of F₁(), F₄( set ) -> set } :

ex F being ManySortedFunctor of F₂(),F₃() st
for a being Element of F₁() holds F . a = F₄(a)

provided

A1: for a being Element of F₁() holds F₄(a) is Functor of F₂() . a,F₃() . a

proof end;

definition

let A be non empty set ;
let F, G be ManySortedCategory of A;
let f be ManySortedFunctor of F,G;
let a be Element of A;
:: original: .
redefine func f . a -> Functor of F . a,G . a;
coherence by Def7;

end;

definition

let A, B be non empty set ;
let F, G be Function of B,A;
mode Indexing of F,G -> Category-yielding_on_first ManySortedSet of A,B means :Def8: :: INDEX_1:def 8
it `2 is ManySortedFunctor of (it `1 ) * F,(it `1 ) * G;
existence

proof end;

end;

:: deftheorem Def8 defines Indexing INDEX_1:def 8 :

theorem Th4: :: INDEX_1:4

for A, B being non empty set
for F, G being Function of B,A
for I being Indexing of F,G
for m being Element of B holds (I `2 ) . m is Functor of (I `1 ) . (F . m),(I `1 ) . (G . m)

proof end;

theorem Th5: :: INDEX_1:5

for C being Category
for I being Indexing of the Dom of C,the Cod of C
for m being Morphism of C holds (I `2 ) . m is Functor of (I `1 ) . (dom m),(I `1 ) . (cod m)

proof end;

definition

let A, B be non empty set ;
let F, G be Function of B,A;
let I be Indexing of F,G;
:: original: `2
redefine func I `2 -> ManySortedFunctor of (I `1 ) * F,(I `1 ) * G;
coherence by Def8;

end;

Lm1: now

let A, B be non empty set ; :: thesis:
let F, G be Function of B,A; :: thesis:
let I be Indexing of F,G; :: thesis:
A1: dom (I `1 ) = A by PBOOLE:def 3;
consider C being strict Categorial full Category such that
A2: the Objects of C = rng (I `1 ) by CAT_5:20;
take C = C; :: thesis:
thus for a being Element of A holds (I `1 ) . a is Object of C by A1, A2, FUNCT_1:def 5; :: thesis:
let b be Element of B; :: thesis:
( (I `1 ) . (F . b) is Object of C & (I `1 ) . (G . b) is Object of C & (I `2 ) . b is Functor of (I `1 ) . (F . b),(I `1 ) . (G . b) ) by A1, A2, Th4, FUNCT_1:def 5;
hence [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C by CAT_5:def 8; :: thesis:

end;

definition

let A, B be non empty set ;
let F, G be Function of B,A;
let I be Indexing of F,G;
mode TargetCat of I -> Categorial Category means :Def9: :: INDEX_1:def 9
( ( for a being Element of A holds (I `1 ) . a is Object of it ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of it ) );
existence

proof end;

end;

:: deftheorem Def9 defines TargetCat INDEX_1:def 9 :

registration

let A, B be non empty set ;
let F, G be Function of B,A;
let I be Indexing of F,G;
cluster strict Categorial full TargetCat of I;
existence

proof end;

end;

Lm2: now

let C be Category; :: thesis:
id C = id the Morphisms of C by CAT_1:def 21;
hence id C = (id C) * (id C) by FUNCT_2:23; :: thesis:

end;

definition

let A, B be non empty set ;
let F, G be Function of B,A;
let c be PartFunc of [:B,B:],B;
let i be Function of A,B;
given C being Category such that A1: C = CatStr(# A,B,F,G,c,i #) ;
mode Indexing of F,G,c,i -> Indexing of F,G means :Def10: :: INDEX_1:def 10
( ( for a being Element of A holds (it `2 ) . (i . a) = id ((it `1 ) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(it `2 ) . (c . [m2,m1]) = ((it `2 ) . m2) * ((it `2 ) . m1) ) );
existence

proof end;

end;

:: deftheorem Def10 defines Indexing INDEX_1:def 10 :

definition

let C be Category;
mode Indexing of C is Indexing of the Dom of C,the Cod of C,the Comp of C,the Id of C;
mode coIndexing of C is Indexing of the Cod of C,the Dom of C, ~ the Comp of C,the Id of C;

end;

theorem Th6: :: INDEX_1:6

for C being Category
for I being Indexing of the Dom of C,the Cod of C holds
( I is Indexing of C iff ( ( for a being Object of C holds (I `2 ) . (id a) = id ((I `1 ) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2 ) . (m2 * m1) = ((I `2 ) . m2) * ((I `2 ) . m1) ) ) )

proof end;

theorem Th7: :: INDEX_1:7

for C being Category
for I being Indexing of the Cod of C,the Dom of C holds
( I is coIndexing of C iff ( ( for a being Object of C holds (I `2 ) . (id a) = id ((I `1 ) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2 ) . (m2 * m1) = ((I `2 ) . m1) * ((I `2 ) . m2) ) ) )

proof end;

theorem :: INDEX_1:8

for C being Category
for x being set holds
( x is coIndexing of C iff x is Indexing of (C opp ) )

proof end;

theorem :: INDEX_1:9

for C being Category
for I being Indexing of C
for c1, c2 being Object of C st not Hom c1,c2 is empty holds
for m being Morphism of c1,c2 holds (I `2 ) . m is Functor of (I `1 ) . c1,(I `1 ) . c2

proof end;

theorem :: INDEX_1:10

for C being Category
for I being coIndexing of C
for c1, c2 being Object of C st not Hom c1,c2 is empty holds
for m being Morphism of c1,c2 holds (I `2 ) . m is Functor of (I `1 ) . c2,(I `1 ) . c1

proof end;

definition

let C be Category;
let I be Indexing of C;
let T be TargetCat of I;
func I -functor C,T -> Functor of C,T means :Def11: :: INDEX_1:def 11
for f being Morphism of C holds it . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines -functor INDEX_1:def 11 :

Lm3: for C being Category
for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor C,T) = I `1

proof end;

theorem Th11: :: INDEX_1:11

for C being Category
for I being Indexing of C
for T1, T2 being TargetCat of I holds
( I -functor C,T1 = I -functor C,T2 & Obj (I -functor C,T1) = Obj (I -functor C,T2) )

proof end;

theorem :: INDEX_1:12

for C being Category
for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor C,T) = I `1 by Lm3;

theorem :: INDEX_1:13

for C being Category
for I being Indexing of C
for T being TargetCat of I
for x being Object of C holds (I -functor C,T) . x = (I `1 ) . x

proof end;

definition

let C be Category;
let I be Indexing of C;
func rng I -> strict TargetCat of I means :Def12: :: INDEX_1:def 12
for T being TargetCat of I holds it = Image (I -functor C,T);
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def12 defines rng INDEX_1:def 12 :

theorem Th14: :: INDEX_1:14

for C being Category
for I being Indexing of C
for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )

proof end;

definition

let C be Category;
let I be Indexing of C;
let m be Morphism of C;
func I . m -> Functor of (I `1 ) . (dom m),(I `1 ) . (cod m) equals :: INDEX_1:def 13
(I `2 ) . m;
coherence

proof end;

end;

:: deftheorem defines . INDEX_1:def 13 :

definition

let C be Category;
let I be coIndexing of C;
let m be Morphism of C;
func I . m -> Functor of (I `1 ) . (cod m),(I `1 ) . (dom m) equals :: INDEX_1:def 14
(I `2 ) . m;
coherence

proof end;

end;

:: deftheorem defines . INDEX_1:def 14 :

Lm4: now

let C, D be Category; :: thesis:
set F = the Objects of C --> D;
set G = the Morphisms of C --> (id D);
set H = [(the Objects of C --> D),(the Morphisms of C --> (id D))];
let m be Morphism of C; :: thesis:
dom (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Dom of C) = the Morphisms of C by PBOOLE:def 3;
then A1: (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Dom of C) . m = ([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) . (the Dom of C . m) by FUNCT_1:22
.= (the Objects of C --> D) . (the Dom of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
dom (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Cod of C) = the Morphisms of C by PBOOLE:def 3;
then A2: (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Cod of C) . m = ([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) . (the Cod of C . m) by FUNCT_1:22
.= (the Objects of C --> D) . (the Cod of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
([(the Objects of C --> D),(the Morphisms of C --> (id D))] `2 ) . m = (the Morphisms of C --> (id D)) . m by MCART_1:7
.= id D by FUNCOP_1:13 ;
hence ([(the Objects of C --> D),(the Morphisms of C --> (id D))] `2 ) . m is Functor of (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Dom of C) . m,(([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Cod of C) . m by A1, A2; :: thesis:

end;

Lm5: now

let C, D be Category; :: thesis:
set F = the Objects of C --> D;
set G = the Morphisms of C --> (id D);
set H = [(the Objects of C --> D),(the Morphisms of C --> (id D))];
let m be Morphism of C; :: thesis:
dom (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Dom of C) = the Morphisms of C by PBOOLE:def 3;
then A1: (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Dom of C) . m = ([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) . (the Dom of C . m) by FUNCT_1:22
.= (the Objects of C --> D) . (the Dom of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
dom (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Cod of C) = the Morphisms of C by PBOOLE:def 3;
then A2: (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Cod of C) . m = ([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) . (the Cod of C . m) by FUNCT_1:22
.= (the Objects of C --> D) . (the Cod of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
([(the Objects of C --> D),(the Morphisms of C --> (id D))] `2 ) . m = (the Morphisms of C --> (id D)) . m by MCART_1:7
.= id D by FUNCOP_1:13 ;
hence ([(the Objects of C --> D),(the Morphisms of C --> (id D))] `2 ) . m is Functor of (([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Cod of C) . m,(([(the Objects of C --> D),(the Morphisms of C --> (id D))] `1 ) * the Dom of C) . m by A1, A2; :: thesis:

end;

theorem :: INDEX_1:15

for C, D being Category holds
( [(the Objects of C --> D),(the Morphisms of C --> (id D))] is Indexing of C & [(the Objects of C --> D),(the Morphisms of C --> (id D))] is coIndexing of C )

proof end;

registration

let C be Category;
let D be Categorial Category;
let F be Functor of C,D;
cluster Obj F -> Category-yielding ;
coherence

proof end;

end;

theorem Th16: :: INDEX_1:16

for C being Category
for D being Categorial Category
for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C

proof end;

definition

let C be Category;
let D be Categorial Category;
let F be Functor of C,D;
func F -indexing_of C -> Indexing of C equals :: INDEX_1:def 15
[(Obj F),(pr2 F)];
coherence by Th16;

end;

:: deftheorem defines -indexing_of INDEX_1:def 15 :

theorem :: INDEX_1:17

for C being Category
for D being Categorial Category
for F being Functor of C,D holds D is TargetCat of F -indexing_of C

proof end;

theorem Th18: :: INDEX_1:18

for C being Category
for D being Categorial Category
for F being Functor of C,D
for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor C,T

proof end;

theorem Th19: :: INDEX_1:19

for C being Category
for D, E being Categorial Category
for F being Functor of C,D
for G being Functor of C,E st F = G holds
F -indexing_of C = G -indexing_of C by Th2;

theorem Th20: :: INDEX_1:20

for C being Category
for I being Indexing of C
for T being TargetCat of I holds pr2 (I -functor C,T) = I `2

proof end;

theorem :: INDEX_1:21

for C being Category
for I being Indexing of C
for T being TargetCat of I holds (I -functor C,T) -indexing_of C = I

proof end;

Lm6: now

let c, d be Category; :: thesis:
let e be Subcategory of d; :: thesis:
let f be Functor of c,e; :: thesis:
(incl e) * f = (id e) * f by CAT_2:def 5
.= (id the Morphisms of e) * f by CAT_1:def 21
.= f by FUNCT_2:23 ;
hence f is Functor of c,d ; :: thesis:

end;

definition

let C, D, E be Category;
let F be Functor of C,D;
let I be Indexing of E;
assume A1: Image F is Subcategory of E ;
func I * F -> Indexing of C means :Def16: :: INDEX_1:def 16
for F' being Functor of C,E st F' = F holds
it = ((I -functor E,(rng I)) * F') -indexing_of C;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines * INDEX_1:def 16 :

theorem Th22: :: INDEX_1:22

for C, D1, D2, E being Category
for I being Indexing of E
for F being Functor of C,D1
for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds
I * F = I * G

proof end;

theorem Th23: :: INDEX_1:23

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I holds I * F = ((I -functor D,T) * F) -indexing_of C

proof end;

theorem Th24: :: INDEX_1:24

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I holds T is TargetCat of I * F

proof end;

theorem :: INDEX_1:25

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I holds rng (I * F) is Subcategory of T

proof end;

theorem Th26: :: INDEX_1:26

for C, D, E being Category
for F being Functor of C,D
for G being Functor of D,E
for I being Indexing of E holds (I * G) * F = I * (G * F)

proof end;

definition

let C be Category;
let I be Indexing of C;
let D be Categorial Category;
assume A1: D is TargetCat of I ;
let E be Categorial Category;
let F be Functor of D,E;
func F * I -> Indexing of C means :Def17: :: INDEX_1:def 17
for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
it = (G * (I -functor C,T)) -indexing_of C;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines * INDEX_1:def 17 :

theorem Th27: :: INDEX_1:27

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of T,E st F = G holds
F * I = G * I

proof end;

theorem Th28: :: INDEX_1:28

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds Image F is TargetCat of F * I

proof end;

theorem Th29: :: INDEX_1:29

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds D is TargetCat of F * I

proof end;

theorem :: INDEX_1:30

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds rng (F * I) is Subcategory of Image F

proof end;

theorem :: INDEX_1:31

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D, E being Categorial Category
for F being Functor of T,D
for G being Functor of D,E holds (G * F) * I = G * (F * I)

proof end;

definition

let C, D be Category;
let I1 be Indexing of C;
let I2 be Indexing of D;
func I2 * I1 -> Indexing of C equals :: INDEX_1:def 18
I2 * (I1 -functor C,(rng I1));
correctness ;

end;

:: deftheorem defines * INDEX_1:def 18 :

theorem Th32: :: INDEX_1:32

for C being Category
for D being Categorial Category
for I1 being Indexing of C
for I2 being Indexing of D
for T being TargetCat of I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor C,T)

proof end;

theorem :: INDEX_1:33

for C being Category
for D being Categorial Category
for I1 being Indexing of C
for I2 being Indexing of D
for T being TargetCat of I2 st D is TargetCat of I1 holds
I2 * I1 = (I2 -functor D,T) * I1

proof end;

theorem Th34: :: INDEX_1:34

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I
for E being Categorial Category
for G being Functor of T,E holds (G * I) * F = G * (I * F)

proof end;

theorem :: INDEX_1:35

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)

proof end;

theorem :: INDEX_1:36

for C being Category
for I being Indexing of C
for T1 being TargetCat of I
for J being Indexing of T1
for T2 being TargetCat of J
for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)

proof end;

theorem Th37: :: INDEX_1:37

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I
for J being Indexing of T holds (J * I) * F = J * (I * F)

proof end;

theorem :: INDEX_1:38

for C being Category
for I being Indexing of C
for D being TargetCat of I
for J being Indexing of D
for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)

proof end;