:: INDEX_1 semantic presentation

registration

let c₁ be non empty set ;
cluster V3 ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster V2 -> V3 ManySortedSet of a₁;
coherence

proof end;

end;

definition

let c₁ be Categorial Category;
let c₂ be Morphism of c₁;
redefine func `2 as c₂ `2 -> Functor of a₂ `11 ,a₂ `12 ;
coherence

proof end;

end;

theorem Th1: :: INDEX_1:1

for b₁ being Categorial Category
for b₂, b₃ being Morphism of b₁ st dom b₃ = cod b₂ holds
b₃ * b₂ = [[(dom b₂),(cod b₃)],((b₃ `2 ) * (b₂ `2 ))]

proof end;

theorem Th2: :: INDEX_1:2

for b₁ being Category
for b₂, b₃ being Categorial Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃ st b₄ = b₅ holds
Obj b₄ = Obj b₅

proof end;

definition

let c₁ be Function;
attr a₁ is Category-yielding means :Def1: :: INDEX_1:def 1
for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ is Category;

end;

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

registration

cluster Category-yielding set ;
existence

proof end;

end;

registration

let c₁ be set ;
cluster Category-yielding ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode ManySortedCategory of a₁ is Category-yielding ManySortedSet of a₁;

end;

definition

let c₁ be Category;
mode ManySortedSet of a₁ is ManySortedSet of the Objects of a₁;
mode ManySortedCategory of a₁ is ManySortedCategory of the Objects of a₁;

end;

registration

let c₁ be set ;
let c₂ be Category;
cluster a₁ --> a₂ -> Category-yielding ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster -> non empty ManySortedSet of a₁;
coherence

proof end;

end;

registration

let c₁ be Category-yielding Function;
cluster rng a₁ -> categorial ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedCategory of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Category;
coherence

proof end;

end;

registration

let c₁ be Function;
let c₂ be Category-yielding Function;
cluster a₁ * a₂ -> Category-yielding ;
coherence

proof end;

end;

definition

let c₁ be Category-yielding Function;
func Objs c₁ -> non-empty Function means :Def2: :: INDEX_1:def 2
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
for b₂ being Category st b₂ = a₁ . b₁ holds
a₂ . b₁ = the Objects of b₂ ) );
existence

proof end;

uniqueness

proof end;

func Mphs c₁ -> non-empty Function means :Def3: :: INDEX_1:def 3
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
for b₂ being Category st b₂ = a₁ . b₁ holds
a₂ . b₁ = the Morphisms of b₂ ) );
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 c₁ be non empty set ;
let c₂ be ManySortedCategory of c₁;
redefine func Objs as Objs c₂ -> V2 ManySortedSet of a₁;
coherence

proof end;

redefine func Mphs as Mphs c₂ -> V2 ManySortedSet of a₁;
coherence

proof end;

end;

theorem Th3: :: INDEX_1:3

for b₁ being set
for b₂ being Category holds
( Objs (b₁ --> b₂) = b₁ --> the Objects of b₂ & Mphs (b₁ --> b₂) = b₁ --> the Morphisms of b₂ )

proof end;

definition

let c₁, c₂ be set ;
mode ManySortedSet of c₁,c₂ -> set means :Def4: :: INDEX_1:def 4
ex b₁ being ManySortedSet of a₁ex b₂ being ManySortedSet of a₂ st a₃ = [b₁,b₂];
existence

proof end;

end;

:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :

definition

let c₁, c₂ be set ;
let c₃ be ManySortedSet of c₁;
let c₄ be ManySortedSet of c₂;
redefine func [ as [c₃,c₄] -> ManySortedSet of a₁,a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be ManySortedSet of c₁,c₂;
redefine func `1 as c₃ `1 -> ManySortedSet of a₁;
coherence

proof end;

redefine func `2 as c₃ `2 -> ManySortedSet of a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be ManySortedSet of c₁,c₂;
attr a₃ is Category-yielding_on_first means :Def5: :: INDEX_1:def 5
a₃ `1 is Category-yielding;
attr a₃ is Function-yielding_on_second means :Def6: :: INDEX_1:def 6
a₃ `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 c₁, c₂ be set ;
cluster Category-yielding_on_first Function-yielding_on_second ManySortedSet of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be Category-yielding_on_first ManySortedSet of c₁,c₂;
redefine func `1 as c₃ `1 -> ManySortedCategory of a₁;
coherence by Def5;

end;

definition

let c₁, c₂ be set ;
let c₃ be Function-yielding_on_second ManySortedSet of c₁,c₂;
redefine func `2 as c₃ `2 -> ManySortedFunction of a₂;
coherence by Def6;

end;

registration

let c₁ be Function-yielding Function;
cluster rng a₁ -> functional ;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be ManySortedCategory of c₁;
let c₄ be ManySortedFunction of c₂;
redefine func [ as [c₃,c₄] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be ManySortedCategory of c₁;
mode ManySortedFunctor of c₂,c₃ -> ManySortedFunction of a₁ means :Def7: :: INDEX_1:def 7
for b₁ being Element of a₁ holds a₄ . b₁ is Functor of a₂ . b₁,a₃ . b₁;
existence

proof end;

end;

:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :

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

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

provided

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

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be ManySortedCategory of c₁;
let c₄ be ManySortedFunctor of c₂,c₃;
let c₅ be Element of c₁;
redefine func . as c₄ . c₅ -> Functor of a₂ . a₅,a₃ . a₅;
coherence by Def7;

end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be Function of c₂,c₁;
mode Indexing of c₃,c₄ -> Category-yielding_on_first ManySortedSet of a₁,a₂ means :Def8: :: INDEX_1:def 8
a₅ `2 is ManySortedFunctor of (a₅ `1 ) * a₃,(a₅ `1 ) * a₄;
existence

proof end;

end;

:: deftheorem Def8 defines Indexing INDEX_1:def 8 :

theorem Th4: :: INDEX_1:4

for b₁, b₂ being non empty set
for b₃, b₄ being Function of b₂,b₁
for b₅ being Indexing of b₃,b₄
for b₆ being Element of b₂ holds (b₅ `2 ) . b₆ is Functor of (b₅ `1 ) . (b₃ . b₆),(b₅ `1 ) . (b₄ . b₆)

proof end;

theorem Th5: :: INDEX_1:5

for b₁ being Category
for b₂ being Indexing of the Dom of b₁,the Cod of b₁
for b₃ being Morphism of b₁ holds (b₂ `2 ) . b₃ is Functor of (b₂ `1 ) . (dom b₃),(b₂ `1 ) . (cod b₃)

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be Function of c₂,c₁;
let c₅ be Indexing of c₃,c₄;
redefine func `2 as c₅ `2 -> ManySortedFunctor of (a₅ `1 ) * a₃,(a₅ `1 ) * a₄;
coherence by Def8;

end;

E12: now

let c₁, c₂ be non empty set ;
let c₃, c₄ be Function of c₂,c₁;
let c₅ be Indexing of c₃,c₄;
E13: dom (c₅ `1 ) = c₁ by PBOOLE:def 3;
consider c₆ being strict Categorial full Category such that
E14: the Objects of c₆ = rng (c₅ `1 ) by CAT_5:20;
take c₇ = c₆;
thus for b₁ being Element of c₁ holds (c₅ `1 ) . b₁ is Object of c₇ by E13, E14, FUNCT_1:def 5;
let c₈ be Element of c₂;
( (c₅ `1 ) . (c₃ . c₈) is Object of c₇ & (c₅ `1 ) . (c₄ . c₈) is Object of c₇ & (c₅ `2 ) . c₈ is Functor of (c₅ `1 ) . (c₃ . c₈),(c₅ `1 ) . (c₄ . c₈) ) by E13, E14, Th4, FUNCT_1:def 5;
hence [[((c₅ `1 ) . (c₃ . c₈)),((c₅ `1 ) . (c₄ . c₈))],((c₅ `2 ) . c₈)] is Morphism of c₇ by CAT_5:def 8;

end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be Function of c₂,c₁;
let c₅ be Indexing of c₃,c₄;
mode TargetCat of c₅ -> Categorial Category means :Def9: :: INDEX_1:def 9
( ( for b₁ being Element of a₁ holds (a₅ `1 ) . b₁ is Object of a₆ ) & ( for b₁ being Element of a₂ holds [[((a₅ `1 ) . (a₃ . b₁)),((a₅ `1 ) . (a₄ . b₁))],((a₅ `2 ) . b₁)] is Morphism of a₆ ) );
existence

proof end;

end;

:: deftheorem Def9 defines TargetCat INDEX_1:def 9 :

registration

let c₁, c₂ be non empty set ;
let c₃, c₄ be Function of c₂,c₁;
let c₅ be Indexing of c₃,c₄;
cluster strict Categorial full TargetCat of a₅;
existence

proof end;

end;

E14: now

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

end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be Function of c₂,c₁;
let c₅ be PartFunc of [:c₂,c₂:],c₂;
let c₆ be Function of c₁,c₂;
given c₇ being Category such that E15: c₇ = CatStr(# c₁,c₂,c₃,c₄,c₅,c₆ #) ;
mode Indexing of c₃,c₄,c₅,c₆ -> Indexing of a₃,a₄ means :Def10: :: INDEX_1:def 10
( ( for b₁ being Element of a₁ holds (a₇ `2 ) . (a₆ . b₁) = id ((a₇ `1 ) . b₁) ) & ( for b₁, b₂ being Element of a₂ st a₃ . b₂ = a₄ . b₁ holds
(a₇ `2 ) . (a₅ . [b₂,b₁]) = ((a₇ `2 ) . b₂) * ((a₇ `2 ) . b₁) ) );
existence

proof end;

end;

:: deftheorem Def10 defines Indexing INDEX_1:def 10 :

definition

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

end;

theorem Th6: :: INDEX_1:6

for b₁ being Category
for b₂ being Indexing of the Dom of b₁,the Cod of b₁ holds
( b₂ is Indexing of b₁ iff ( ( for b₃ being Object of b₁ holds (b₂ `2 ) . (id b₃) = id ((b₂ `1 ) . b₃) ) & ( for b₃, b₄ being Morphism of b₁ st dom b₄ = cod b₃ holds
(b₂ `2 ) . (b₄ * b₃) = ((b₂ `2 ) . b₄) * ((b₂ `2 ) . b₃) ) ) )

proof end;

theorem Th7: :: INDEX_1:7

for b₁ being Category
for b₂ being Indexing of the Cod of b₁,the Dom of b₁ holds
( b₂ is coIndexing of b₁ iff ( ( for b₃ being Object of b₁ holds (b₂ `2 ) . (id b₃) = id ((b₂ `1 ) . b₃) ) & ( for b₃, b₄ being Morphism of b₁ st dom b₄ = cod b₃ holds
(b₂ `2 ) . (b₄ * b₃) = ((b₂ `2 ) . b₃) * ((b₂ `2 ) . b₄) ) ) )

proof end;

theorem Th8: :: INDEX_1:8

for b₁ being Category
for b₂ being set holds
( b₂ is coIndexing of b₁ iff b₂ is Indexing of (b₁ opp ) )

proof end;

theorem Th9: :: INDEX_1:9

for b₁ being Category
for b₂ being Indexing of b₁
for b₃, b₄ being Object of b₁ st not Hom b₃,b₄ is empty holds
for b₅ being Morphism of b₃,b₄ holds (b₂ `2 ) . b₅ is Functor of (b₂ `1 ) . b₃,(b₂ `1 ) . b₄

proof end;

theorem Th10: :: INDEX_1:10

for b₁ being Category
for b₂ being coIndexing of b₁
for b₃, b₄ being Object of b₁ st not Hom b₃,b₄ is empty holds
for b₅ being Morphism of b₃,b₄ holds (b₂ `2 ) . b₅ is Functor of (b₂ `1 ) . b₄,(b₂ `1 ) . b₃

proof end;

definition

let c₁ be Category;
let c₂ be Indexing of c₁;
let c₃ be TargetCat of c₂;
func c₂ -functor c₁,c₃ -> Functor of a₁,a₃ means :Def11: :: INDEX_1:def 11
for b₁ being Morphism of a₁ holds a₄ . b₁ = [[((a₂ `1 ) . (dom b₁)),((a₂ `1 ) . (cod b₁))],((a₂ `2 ) . b₁)];
existence

proof end;

uniqueness

proof end;

end;

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

Lemma19: for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂ holds Obj (b₂ -functor b₁,b₃) = b₂ `1

proof end;

theorem Th11: :: INDEX_1:11

for b₁ being Category
for b₂ being Indexing of b₁
for b₃, b₄ being TargetCat of b₂ holds
( b₂ -functor b₁,b₃ = b₂ -functor b₁,b₄ & Obj (b₂ -functor b₁,b₃) = Obj (b₂ -functor b₁,b₄) )

proof end;

theorem Th12: :: INDEX_1:12

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂ holds Obj (b₂ -functor b₁,b₃) = b₂ `1 by Lemma19;

theorem Th13: :: INDEX_1:13

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Object of b₁ holds (b₂ -functor b₁,b₃) . b₄ = (b₂ `1 ) . b₄

proof end;

definition

let c₁ be Category;
let c₂ be Indexing of c₁;
func rng c₂ -> strict TargetCat of a₂ means :Def12: :: INDEX_1:def 12
for b₁ being TargetCat of a₂ holds a₃ = Image (a₂ -functor a₁,b₁);
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def12 defines rng INDEX_1:def 12 :

theorem Th14: :: INDEX_1:14

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being Categorial Category holds
( rng b₂ is Subcategory of b₃ iff b₃ is TargetCat of b₂ )

proof end;

definition

let c₁ be Category;
let c₂ be Indexing of c₁;
let c₃ be Morphism of c₁;
func c₂ . c₃ -> Functor of (a₂ `1 ) . (dom a₃),(a₂ `1 ) . (cod a₃) equals :: INDEX_1:def 13
(a₂ `2 ) . a₃;
coherence

proof end;

end;

:: deftheorem Def13 defines . INDEX_1:def 13 :

definition

let c₁ be Category;
let c₂ be coIndexing of c₁;
let c₃ be Morphism of c₁;
func c₂ . c₃ -> Functor of (a₂ `1 ) . (cod a₃),(a₂ `1 ) . (dom a₃) equals :: INDEX_1:def 14
(a₂ `2 ) . a₃;
coherence

proof end;

end;

:: deftheorem Def14 defines . INDEX_1:def 14 :

E23: now

let c₁, c₂ be Category;
set c₃ = the Objects of c₁ --> c₂;
set c₄ = the Morphisms of c₁ --> (id c₂);
set c₅ = [(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))];
let c₆ be Morphism of c₁;
dom (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Dom of c₁) = the Morphisms of c₁ by PBOOLE:def 3;
then E24: (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Dom of c₁) . c₆ = ([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) . (the Dom of c₁ . c₆) by FUNCT_1:22
.= (the Objects of c₁ --> c₂) . (the Dom of c₁ . c₆) by MCART_1:7
.= c₂ by FUNCOP_1:13 ;
dom (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Cod of c₁) = the Morphisms of c₁ by PBOOLE:def 3;
then E25: (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Cod of c₁) . c₆ = ([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) . (the Cod of c₁ . c₆) by FUNCT_1:22
.= (the Objects of c₁ --> c₂) . (the Cod of c₁ . c₆) by MCART_1:7
.= c₂ by FUNCOP_1:13 ;
([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `2 ) . c₆ = (the Morphisms of c₁ --> (id c₂)) . c₆ by MCART_1:7
.= id c₂ by FUNCOP_1:13 ;
hence ([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `2 ) . c₆ is Functor of (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Dom of c₁) . c₆,(([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Cod of c₁) . c₆ by E24, E25;

end;

E24: now

let c₁, c₂ be Category;
set c₃ = the Objects of c₁ --> c₂;
set c₄ = the Morphisms of c₁ --> (id c₂);
set c₅ = [(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))];
let c₆ be Morphism of c₁;
dom (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Dom of c₁) = the Morphisms of c₁ by PBOOLE:def 3;
then E25: (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Dom of c₁) . c₆ = ([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) . (the Dom of c₁ . c₆) by FUNCT_1:22
.= (the Objects of c₁ --> c₂) . (the Dom of c₁ . c₆) by MCART_1:7
.= c₂ by FUNCOP_1:13 ;
dom (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Cod of c₁) = the Morphisms of c₁ by PBOOLE:def 3;
then E26: (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Cod of c₁) . c₆ = ([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) . (the Cod of c₁ . c₆) by FUNCT_1:22
.= (the Objects of c₁ --> c₂) . (the Cod of c₁ . c₆) by MCART_1:7
.= c₂ by FUNCOP_1:13 ;
([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `2 ) . c₆ = (the Morphisms of c₁ --> (id c₂)) . c₆ by MCART_1:7
.= id c₂ by FUNCOP_1:13 ;
hence ([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `2 ) . c₆ is Functor of (([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Cod of c₁) . c₆,(([(the Objects of c₁ --> c₂),(the Morphisms of c₁ --> (id c₂))] `1 ) * the Dom of c₁) . c₆ by E25, E26;

end;

theorem Th15: :: INDEX_1:15

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

proof end;

registration

let c₁ be Category;
let c₂ be Categorial Category;
let c₃ be Functor of c₁,c₂;
cluster Obj a₃ -> Category-yielding ;
coherence

proof end;

end;

theorem Th16: :: INDEX_1:16

for b₁ being Category
for b₂ being Categorial Category
for b₃ being Functor of b₁,b₂ holds [(Obj b₃),(pr2 b₃)] is Indexing of b₁

proof end;

definition

let c₁ be Category;
let c₂ be Categorial Category;
let c₃ be Functor of c₁,c₂;
func c₃ -indexing_of c₁ -> Indexing of a₁ equals :: INDEX_1:def 15
[(Obj a₃),(pr2 a₃)];
coherence by Th16;

end;

:: deftheorem Def15 defines -indexing_of INDEX_1:def 15 :

theorem Th17: :: INDEX_1:17

for b₁ being Category
for b₂ being Categorial Category
for b₃ being Functor of b₁,b₂ holds b₂ is TargetCat of b₃ -indexing_of b₁

proof end;

theorem Th18: :: INDEX_1:18

for b₁ being Category
for b₂ being Categorial Category
for b₃ being Functor of b₁,b₂
for b₄ being TargetCat of b₃ -indexing_of b₁ holds b₃ = (b₃ -indexing_of b₁) -functor b₁,b₄

proof end;

theorem Th19: :: INDEX_1:19

for b₁ being Category
for b₂, b₃ being Categorial Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃ st b₄ = b₅ holds
b₄ -indexing_of b₁ = b₅ -indexing_of b₁ by Th2;

theorem Th20: :: INDEX_1:20

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂ holds pr2 (b₂ -functor b₁,b₃) = b₂ `2

proof end;

theorem Th21: :: INDEX_1:21

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂ holds (b₂ -functor b₁,b₃) -indexing_of b₁ = b₂

proof end;

E29: now

let c₁, c₂ be Category;
let c₃ be Subcategory of c₂;
let c₄ be Functor of c₁,c₃;
(incl c₃) * c₄ = (id c₃) * c₄ by CAT_2:def 5
.= (id the Morphisms of c₃) * c₄ by CAT_1:def 21
.= c₄ by FUNCT_2:23 ;
hence c₄ is Functor of c₁,c₂ ;

end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₂;
let c₅ be Indexing of c₃;
assume E30: Image c₄ is Subcategory of c₃ ;
func c₅ * c₄ -> Indexing of a₁ means :Def16: :: INDEX_1:def 16
for b₁ being Functor of a₁,a₃ st b₁ = a₄ holds
a₆ = ((a₅ -functor a₃,(rng a₅)) * b₁) -indexing_of a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines * INDEX_1:def 16 :

theorem Th22: :: INDEX_1:22

for b₁, b₂, b₃, b₄ being Category
for b₅ being Indexing of b₄
for b₆ being Functor of b₁,b₂
for b₇ being Functor of b₁,b₃ st Image b₆ is Subcategory of b₄ & Image b₇ is Subcategory of b₄ & b₆ = b₇ holds
b₅ * b₆ = b₅ * b₇

proof end;

theorem Th23: :: INDEX_1:23

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₄ holds b₄ * b₃ = ((b₄ -functor b₂,b₅) * b₃) -indexing_of b₁

proof end;

theorem Th24: :: INDEX_1:24

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₄ holds b₅ is TargetCat of b₄ * b₃

proof end;

theorem Th25: :: INDEX_1:25

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₄ holds rng (b₄ * b₃) is Subcategory of b₅

proof end;

theorem Th26: :: INDEX_1:26

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₂,b₃
for b₆ being Indexing of b₃ holds (b₆ * b₅) * b₄ = b₆ * (b₅ * b₄)

proof end;

definition

let c₁ be Category;
let c₂ be Indexing of c₁;
let c₃ be Categorial Category;
assume E35: c₃ is TargetCat of c₂ ;
let c₄ be Categorial Category;
let c₅ be Functor of c₃,c₄;
func c₅ * c₂ -> Indexing of a₁ means :Def17: :: INDEX_1:def 17
for b₁ being TargetCat of a₂
for b₂ being Functor of b₁,a₄ st b₁ = a₃ & b₂ = a₅ holds
a₆ = (b₂ * (a₂ -functor a₁,b₁)) -indexing_of a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines * INDEX_1:def 17 :

theorem Th27: :: INDEX_1:27

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄, b₅ being Categorial Category
for b₆ being Functor of b₃,b₄
for b₇ being Functor of b₃,b₅ st b₆ = b₇ holds
b₆ * b₂ = b₇ * b₂

proof end;

theorem Th28: :: INDEX_1:28

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Categorial Category
for b₅ being Functor of b₃,b₄ holds Image b₅ is TargetCat of b₅ * b₂

proof end;

theorem Th29: :: INDEX_1:29

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Categorial Category
for b₅ being Functor of b₃,b₄ holds b₄ is TargetCat of b₅ * b₂

proof end;

theorem Th30: :: INDEX_1:30

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Categorial Category
for b₅ being Functor of b₃,b₄ holds rng (b₅ * b₂) is Subcategory of Image b₅

proof end;

theorem Th31: :: INDEX_1:31

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄, b₅ being Categorial Category
for b₆ being Functor of b₃,b₄
for b₇ being Functor of b₄,b₅ holds (b₇ * b₆) * b₂ = b₇ * (b₆ * b₂)

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Indexing of c₁;
let c₄ be Indexing of c₂;
func c₄ * c₃ -> Indexing of a₁ equals :: INDEX_1:def 18
a₄ * (a₃ -functor a₁,(rng a₃));
correctness ;

end;

:: deftheorem Def18 defines * INDEX_1:def 18 :

theorem Th32: :: INDEX_1:32

for b₁ being Category
for b₂ being Categorial Category
for b₃ being Indexing of b₁
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₃ st b₂ is TargetCat of b₃ holds
b₄ * b₃ = b₄ * (b₃ -functor b₁,b₅)

proof end;

theorem Th33: :: INDEX_1:33

for b₁ being Category
for b₂ being Categorial Category
for b₃ being Indexing of b₁
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₄ st b₂ is TargetCat of b₃ holds
b₄ * b₃ = (b₄ -functor b₂,b₅) * b₃

proof end;

theorem Th34: :: INDEX_1:34

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₄
for b₆ being Categorial Category
for b₇ being Functor of b₅,b₆ holds (b₇ * b₄) * b₃ = b₇ * (b₄ * b₃)

proof end;

theorem Th35: :: INDEX_1:35

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Categorial Category
for b₅ being Functor of b₃,b₄
for b₆ being Indexing of b₄ holds (b₆ * b₅) * b₂ = b₆ * (b₅ * b₂)

proof end;

theorem Th36: :: INDEX_1:36

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Indexing of b₃
for b₅ being TargetCat of b₄
for b₆ being Categorial Category
for b₇ being Functor of b₅,b₆ holds (b₇ * b₄) * b₂ = b₇ * (b₄ * b₂)

proof end;

theorem Th37: :: INDEX_1:37

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Indexing of b₂
for b₅ being TargetCat of b₄
for b₆ being Indexing of b₅ holds (b₆ * b₄) * b₃ = b₆ * (b₄ * b₃)

proof end;

theorem Th38: :: INDEX_1:38

for b₁ being Category
for b₂ being Indexing of b₁
for b₃ being TargetCat of b₂
for b₄ being Indexing of b₃
for b₅ being TargetCat of b₄
for b₆ being Indexing of b₅ holds (b₆ * b₄) * b₂ = b₆ * (b₄ * b₂)

proof end;