:: INDEX_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let A be non empty set ;
cluster V3 ManySortedSet of A;
existence
not for b1 being ManySortedSet of A holds b1 is empty-yielding
proof end;
end;

registration
let A be non empty set ;
cluster V2 -> V3 ManySortedSet of A;
coherence
for b1 being ManySortedSet of A st b1 is non-empty holds
not b1 is empty-yielding
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
f `2 is Functor of f `11 ,f `12
proof end;
end;

theorem :: INDEX_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for IT being Function holds
( IT is Category-yielding iff for x being set st x in dom IT holds
IT . x is Category );

registration
cluster Category-yielding set ;
existence
ex b1 being Function st b1 is Category-yielding
proof end;
end;

registration
let X be set ;
cluster Category-yielding ManySortedSet of X;
existence
ex b1 being ManySortedSet of X st b1 is Category-yielding
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
X --> x is Category-yielding
proof end;
end;

registration
let X be non empty set ;
cluster -> non empty ManySortedSet of X;
coherence
for b1 being ManySortedSet of X holds not b1 is empty
proof end;
end;

registration
let f be Category-yielding Function;
cluster rng f -> categorial ;
coherence
rng f is categorial
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
f . x is Category
proof end;
end;

registration
let f be Function;
let g be Category-yielding Function;
cluster f * g -> Category-yielding ;
coherence
g * f is Category-yielding
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
ex b1 being non-empty Function st
( dom b1 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the Objects of C ) )
proof end;
uniqueness
for b1, b2 being non-empty Function st dom b1 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the Objects of C ) & dom b2 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the Objects of C ) holds
b1 = b2
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
ex b1 being non-empty Function st
( dom b1 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the Morphisms of C ) )
proof end;
uniqueness
for b1, b2 being non-empty Function st dom b1 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the Morphisms of C ) & dom b2 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the Morphisms of C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Objs INDEX_1:def 2 :
for F being Category-yielding Function
for b2 being non-empty Function holds
( b2 = Objs F iff ( dom b2 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the Objects of C ) ) );

:: deftheorem Def3 defines Mphs INDEX_1:def 3 :
for F being Category-yielding Function
for b2 being non-empty Function holds
( b2 = Mphs F iff ( dom b2 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the Morphisms of C ) ) );

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

theorem :: INDEX_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being set ex f being ManySortedSet of A ex g being ManySortedSet of B st b1 = [f,g]
proof end;
end;

:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :
for A, B being set
for b3 being set holds
( b3 is ManySortedSet of A,B iff ex f being ManySortedSet of A ex g being ManySortedSet of B st b3 = [f,g] );

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
[f,g] is ManySortedSet of A,B
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
X `1 is ManySortedSet of A
proof end;
:: original: `2
redefine func X `2 -> ManySortedSet of B;
coherence
X `2 is ManySortedSet of B
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 :
for A, B being set
for IT being ManySortedSet of A,B holds
( IT is Category-yielding_on_first iff IT `1 is Category-yielding );

:: deftheorem Def6 defines Function-yielding_on_second INDEX_1:def 6 :
for A, B being set
for IT being ManySortedSet of A,B holds
( IT is Function-yielding_on_second iff IT `2 is Function-yielding );

registration
let A, B be set ;
cluster Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;
existence
ex b1 being ManySortedSet of A,B st
( b1 is Category-yielding_on_first & b1 is Function-yielding_on_second )
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
X `1 is ManySortedCategory of A
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
X `2 is ManySortedFunction of B
by Def6;
end;

registration
let f be Function-yielding Function;
cluster rng f -> functional ;
coherence
rng f is functional
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
[f,g] is Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B
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
ex b1 being ManySortedFunction of A st
for a being Element of A holds b1 . a is Functor of F . a,G . a
proof end;
end;

:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :
for A being non empty set
for F, G being ManySortedCategory of A
for b4 being ManySortedFunction of A holds
( b4 is ManySortedFunctor of F,G iff for a being Element of A holds b4 . a is Functor of F . a,G . a );

scheme :: INDEX_1:sch 1
LambdaMSFr{ F1() -> non empty set , F2() -> ManySortedCategory of F1(), F3() -> ManySortedCategory of F1(), F4( set ) -> set } :
ex F being ManySortedFunctor of F2(),F3() st
for a being Element of F1() holds F . a = F4(a)
provided
A1: for a being Element of F1() holds F4(a) is Functor of F2() . a,F3() . 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
f . a is Functor of F . a,G . a
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
ex b1 being Category-yielding_on_first ManySortedSet of A,B st b1 `2 is ManySortedFunctor of (b1 `1 ) * F,(b1 `1 ) * G
proof end;
end;

:: deftheorem Def8 defines Indexing INDEX_1:def 8 :
for A, B being non empty set
for F, G being Function of B,A
for b5 being Category-yielding_on_first ManySortedSet of A,B holds
( b5 is Indexing of F,G iff b5 `2 is ManySortedFunctor of (b5 `1 ) * F,(b5 `1 ) * G );

theorem Th4: :: INDEX_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
I `2 is ManySortedFunctor of (I `1 ) * F,(I `1 ) * G
by Def8;
end;

Lm1: now
let A, B be non empty set ; :: thesis: for F, G being Function of B,A
for I being Indexing of F,G ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1 ) . a is Object of C ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C ) )

let F, G be Function of B,A; :: thesis: for I being Indexing of F,G ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1 ) . a is Object of C ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C ) )

let I be Indexing of F,G; :: thesis: ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1 ) . a is Object of C ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C ) )

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: ( ( for a being Element of A holds (I `1 ) . a is Object of C ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C ) )
thus for a being Element of A holds (I `1 ) . a is Object of C by A1, A2, FUNCT_1:def 5; :: thesis: for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C
let b be Element of B; :: thesis: [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of C
( (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: verum
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
ex b1 being Categorial Category st
( ( for a being Element of A holds (I `1 ) . a is Object of b1 ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of b1 ) )
proof end;
end;

:: deftheorem Def9 defines TargetCat INDEX_1:def 9 :
for A, B being non empty set
for F, G being Function of B,A
for I being Indexing of F,G
for b6 being Categorial Category holds
( b6 is TargetCat of I iff ( ( for a being Element of A holds (I `1 ) . a is Object of b6 ) & ( for b being Element of B holds [[((I `1 ) . (F . b)),((I `1 ) . (G . b))],((I `2 ) . b)] is Morphism of b6 ) ) );

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
ex b1 being TargetCat of I st
( b1 is full & b1 is strict )
proof end;
end;

Lm2: now
let C be Category; :: thesis: id C = (id C) * (id C)
id C = id the Morphisms of C by CAT_1:def 21;
hence id C = (id C) * (id C) by FUNCT_2:23; :: thesis: verum
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
ex b1 being Indexing of F,G st
( ( for a being Element of A holds (b1 `2 ) . (i . a) = id ((b1 `1 ) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b1 `2 ) . (c . [m2,m1]) = ((b1 `2 ) . m2) * ((b1 `2 ) . m1) ) )
proof end;
end;

:: deftheorem Def10 defines Indexing INDEX_1:def 10 :
for A, B being non empty set
for F, G being Function of B,A
for c being PartFunc of [:B,B:],B
for i being Function of A,B st ex C being Category st C = CatStr(# A,B,F,G,c,i #) holds
for b7 being Indexing of F,G holds
( b7 is Indexing of F,G,c,i iff ( ( for a being Element of A holds (b7 `2 ) . (i . a) = id ((b7 `1 ) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b7 `2 ) . (c . [m2,m1]) = ((b7 `2 ) . m2) * ((b7 `2 ) . m1) ) ) );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Functor of C,T st
for f being Morphism of C holds b1 . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)]
proof end;
uniqueness
for b1, b2 being Functor of C,T st ( for f being Morphism of C holds b1 . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)] ) & ( for f being Morphism of C holds b2 . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines -functor INDEX_1:def 11 :
for C being Category
for I being Indexing of C
for T being TargetCat of I
for b4 being Functor of C,T holds
( b4 = I -functor C,T iff for f being Morphism of C holds b4 . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)] );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
for b1, b2 being strict TargetCat of I st ( for T being TargetCat of I holds b1 = Image (I -functor C,T) ) & ( for T being TargetCat of I holds b2 = Image (I -functor C,T) ) holds
b1 = b2
proof end;
existence
ex b1 being strict TargetCat of I st
for T being TargetCat of I holds b1 = Image (I -functor C,T)
proof end;
end;

:: deftheorem Def12 defines rng INDEX_1:def 12 :
for C being Category
for I being Indexing of C
for b3 being strict TargetCat of I holds
( b3 = rng I iff for T being TargetCat of I holds b3 = Image (I -functor C,T) );

theorem Th14: :: INDEX_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
(I `2 ) . m is Functor of (I `1 ) . (dom m),(I `1 ) . (cod m)
proof end;
end;

:: deftheorem defines . INDEX_1:def 13 :
for C being Category
for I being Indexing of C
for m being Morphism of C holds I . m = (I `2 ) . m;

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
(I `2 ) . m is Functor of (I `1 ) . (cod m),(I `1 ) . (dom m)
proof end;
end;

:: deftheorem defines . INDEX_1:def 14 :
for C being Category
for I being coIndexing of C
for m being Morphism of C holds I . m = (I `2 ) . m;

Lm4: now
let C, D be Category; :: thesis: for m being Morphism of C holds ([(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
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: ([(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
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: verum
end;

Lm5: now
let C, D be Category; :: thesis: for m being Morphism of C holds ([(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
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: ([(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
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: verum
end;

theorem :: INDEX_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
Obj F is Category-yielding
proof end;
end;

theorem Th16: :: INDEX_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
[(Obj F),(pr2 F)] is Indexing of C
by Th16;
end;

:: deftheorem defines -indexing_of INDEX_1:def 15 :
for C being Category
for D being Categorial Category
for F being Functor of C,D holds F -indexing_of C = [(Obj F),(pr2 F)];

theorem :: INDEX_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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: for e being Subcategory of d
for f being Functor of c,e holds f is Functor of c,d

let e be Subcategory of d; :: thesis: for f being Functor of c,e holds f is Functor of c,d
let f be Functor of c,e; :: thesis: f is Functor of c,d
(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: verum
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
ex b1 being Indexing of C st
for F' being Functor of C,E st F' = F holds
b1 = ((I -functor E,(rng I)) * F') -indexing_of C
proof end;
uniqueness
for b1, b2 being Indexing of C st ( for F' being Functor of C,E st F' = F holds
b1 = ((I -functor E,(rng I)) * F') -indexing_of C ) & ( for F' being Functor of C,E st F' = F holds
b2 = ((I -functor E,(rng I)) * F') -indexing_of C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines * INDEX_1:def 16 :
for C, D, E being Category
for F being Functor of C,D
for I being Indexing of E st Image F is Subcategory of E holds
for b6 being Indexing of C holds
( b6 = I * F iff for F' being Functor of C,E st F' = F holds
b6 = ((I -functor E,(rng I)) * F') -indexing_of C );

theorem Th22: :: INDEX_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Indexing of C st
for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b1 = (G * (I -functor C,T)) -indexing_of C
proof end;
uniqueness
for b1, b2 being Indexing of C st ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b1 = (G * (I -functor C,T)) -indexing_of C ) & ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b2 = (G * (I -functor C,T)) -indexing_of C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines * INDEX_1:def 17 :
for C being Category
for I being Indexing of C
for D being Categorial Category st D is TargetCat of I holds
for E being Categorial Category
for F being Functor of D,E
for b6 being Indexing of C holds
( b6 = F * I iff for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b6 = (G * (I -functor C,T)) -indexing_of C );

theorem Th27: :: INDEX_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
I2 * (I1 -functor C,(rng I1)) is Indexing of C
;
;
end;

:: deftheorem defines * INDEX_1:def 18 :
for C, D being Category
for I1 being Indexing of C
for I2 being Indexing of D holds I2 * I1 = I2 * (I1 -functor C,(rng I1));

theorem Th32: :: INDEX_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;