:: INDEX_1 semantic presentation

begin

registration
let A be non empty set ;
cluster non empty Relation-like V9() A -defined Function-like total for set ;
existence
 not for b1 being ManySortedSet of A holds b1 is V9()
proof
take  the V8() ManySortedSet of A ; ::_thesis: the V8() ManySortedSet of A is V9()
take  the Element of A ; :: according to PBOOLE:def_12 ::_thesis: ( the Element of A in A & not the V8() ManySortedSet of A . the Element of A is empty )
thus  ( the Element of A in A & not the V8() ManySortedSet of A . the Element of A is empty ) ; ::_thesis: verum
end;
end;

definition
let C be Categorial Category;
let f be Morphism of C;
:: original: `2
redefine funcf `2  ->  Functor of f `11 ,f `12 ;
coherence
 f `2 is Functor of f `11 ,f `12
proof
A1: dom f = f `11 by CAT_5:2;
 ( f `11 = cat (f `11) & f `12 = cat (f `12) ) by CAT_5:def_7;
hence  f `2 is Functor of f `11 ,f `12 by A1, CAT_5:2; ::_thesis: verum
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
let C be Categorial Category; ::_thesis: for f, g being Morphism of C st dom g = cod f holds
g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))]
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))] )
A1: g `11 = dom g by CAT_5:13;
A2: f `11 = dom f by CAT_5:13;
assume A3: dom g = cod f ; ::_thesis: g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))]
then consider ff being Functor of f `11 ,g `11  such that
A4: f = [[(dom f),(cod f)],ff] by A1, A2, CAT_5:def_6;
A5: g `12 = cod g by CAT_5:13;
then consider gg being Functor of g `11 ,g `12  such that
A6: g = [[(dom g),(cod g)],gg] by A1, CAT_5:def_6;
thus g (*) f = [[(dom f),(cod g)],(gg * ff)] by A3, A1, A5, A2, A6, A4, CAT_5:def_6
.= [[(dom f),(cod g)],(gg * (f `2))] by A4, MCART_1:7
.= [[(dom f),(cod g)],((g `2) * (f `2))] by A6, MCART_1:7 ; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let D, E be Categorial Category; ::_thesis: for F being Functor of C,D
for G being Functor of C,E st F = G holds
Obj F = Obj G
let F be Functor of C,D; ::_thesis: for G being Functor of C,E st F = G holds
Obj F = Obj G
let G be Functor of C,E; ::_thesis: ( F = G implies Obj F = Obj G )
assume A1: F = G ; ::_thesis: Obj F = Obj G
A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_C_holds_
(Obj_F)_._x_=_(Obj_G)_._x
let x be set ; ::_thesis: ( x in the carrier of C implies (Obj F) . x = (Obj G) . x )
assume  x in the carrier of C ; ::_thesis: (Obj F) . x = (Obj G) . x
then reconsider a = x as Object of C ;
A3: a = dom (id a) ;
hence (Obj F) . x = dom (F . (id a)) by CAT_1:69
.= (F . (id a)) `11 by CAT_5:13
.= dom (G . (id a)) by A1, CAT_5:13
.= (Obj G) . x by A3, CAT_1:69 ;
::_thesis: verum
end;
 ( dom (Obj F) = the carrier of C & dom (Obj G) = the carrier of C ) by FUNCT_2:def_1;
hence  Obj F = Obj G by A2, FUNCT_1:2; ::_thesis: verum
end;

definition
let IT be Function;
attrIT 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 Relation-like Function-like Category-yielding for set ;
existence
 ex b1 being Function st b1 is Category-yielding
proof
take f = {} --> (1Cat ({},1)); ::_thesis: f is Category-yielding
let x be set ; :: according to INDEX_1:def_1 ::_thesis: ( x in dom f implies f . x is Category )
assume  x in dom f ; ::_thesis: f . x is Category
hence  f . x is Category ; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster Relation-like X -defined Function-like total Category-yielding for set ;
existence
 ex b1 being ManySortedSet of X st b1 is Category-yielding
proof
take f = X --> (1Cat ({},1)); ::_thesis: f is Category-yielding
let x be set ; :: according to INDEX_1:def_1 ::_thesis: ( x in dom f implies f . x is Category )
assume  x in dom f ; ::_thesis: f . x is Category
then  x in X by FUNCOP_1:13;
hence  f . x is Category by FUNCOP_1:7; ::_thesis: verum
end;
end;

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

definition
let C be Category;
mode ManySortedCategory of C is ManySortedCategory of the carrier of C;
end;

registration
let X be set ;
let x be Category;
clusterX --> x ->  Category-yielding ;
coherence
 X --> x is Category-yielding
proof
let a be set ; :: according to INDEX_1:def_1 ::_thesis: ( a in dom (X --> x) implies (X --> x) . a is Category )
assume  a in dom (X --> x) ; ::_thesis: (X --> x) . a is Category
then  a in X by FUNCOP_1:13;
hence  (X --> x) . a is Category by FUNCOP_1:7; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total  ->  non empty for set ;
coherence
 for b1 being ManySortedSet of X holds not b1 is empty ;
end;

registration
let f be Category-yielding Function;
cluster proj2 f ->  categorial ;
coherence
 rng f is categorial
proof
let x be set ; :: according to CAT_5:def_4 ::_thesis: ( not x in rng f or x is CatStr )
assume  x in rng f ; ::_thesis: x is CatStr
then  ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def_3;
hence  x is CatStr by Def1; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let f be ManySortedCategory of X;
let x be Element of X;
:: original: .
redefine funcf . x ->  Category;
coherence
 f . x is Category
proof
 dom f = X by PARTFUN1:def_2;
hence  f . x is Category by Def1; ::_thesis: verum
end;
end;

registration
let f be Function;
let g be Category-yielding Function;
clusterf * g ->  Category-yielding ;
coherence
 g * f is Category-yielding
proof
let x be set ; :: according to INDEX_1:def_1 ::_thesis: ( x in dom (g * f) implies (g * f) . x is Category )
assume  x in dom (g * f) ; ::_thesis: (g * f) . x is Category
then  ( (g * f) . x = g . (f . x) & f . x in dom g ) by FUNCT_1:11, FUNCT_1:12;
hence  (g * f) . x is Category by Def1; ::_thesis: verum
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 carrier 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 carrier of C ) )
proof
defpred S1[ set , set ] means  for C being Category st C = F . $1 holds
$2 = the carrier of C;
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
ex_y_being_set_st_S1[x,y]
let x be set ; ::_thesis: ( x in dom F implies ex y being set st S1[x,y] )
assume  x in dom F ; ::_thesis: ex y being set st S1[x,y]
then reconsider C = F . x as Category by Def1;
reconsider y = the carrier of C as set ;
take y = y; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = dom F & ( for x being set st x in dom F holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
 f is non-empty
proof
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in proj1 f or not f . x is empty )
assume A3: x in dom f ; ::_thesis: not f . x is empty
then reconsider C = F . x as Category by A2, Def1;
 f . x = the carrier of C by A2, A3;
hence  not f . x is empty ; ::_thesis: verum
end;
hence  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 carrier of C ) ) by A2; ::_thesis: verum
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 carrier 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 carrier of C ) holds
b1 = b2
proof
let f1, f2 be non-empty Function; ::_thesis: ( dom f1 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
f1 . x = the carrier of C ) & dom f2 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
f2 . x = the carrier of C ) implies f1 = f2 )
assume that
A4: dom f1 = dom F and
A5: for x being set st x in dom F holds
for C being Category st C = F . x holds
f1 . x = the carrier of C and
A6: dom f2 = dom F and
A7: for x being set st x in dom F holds
for C being Category st C = F . x holds
f2 . x = the carrier of C ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom F implies f1 . x = f2 . x )
assume A8: x in dom F ; ::_thesis: f1 . x = f2 . x
then reconsider C = F . x as Category by Def1;
thus f1 . x = the carrier of C by A5, A8
.= f2 . x by A7, A8 ; ::_thesis: verum
end;
hence  f1 = f2 by A4, A6, FUNCT_1:2; ::_thesis: verum
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 carrier' 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 carrier' of C ) )
proof
defpred S1[ set , set ] means  for C being Category st C = F . $1 holds
$2 = the carrier' of C;
A9: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
ex_y_being_set_st_S1[x,y]
let x be set ; ::_thesis: ( x in dom F implies ex y being set st S1[x,y] )
assume  x in dom F ; ::_thesis: ex y being set st S1[x,y]
then reconsider C = F . x as Category by Def1;
reconsider y = the carrier' of C as set ;
take y = y; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A10: ( dom f = dom F & ( for x being set st x in dom F holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A9);
 f is non-empty
proof
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in proj1 f or not f . x is empty )
assume A11: x in dom f ; ::_thesis: not f . x is empty
then reconsider C = F . x as Category by A10, Def1;
 f . x = the carrier' of C by A10, A11;
hence  not f . x is empty ; ::_thesis: verum
end;
hence  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 carrier' of C ) ) by A10; ::_thesis: verum
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 carrier' 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 carrier' of C ) holds
b1 = b2
proof
let f1, f2 be non-empty Function; ::_thesis: ( dom f1 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
f1 . x = the carrier' of C ) & dom f2 = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
f2 . x = the carrier' of C ) implies f1 = f2 )
assume that
A12: dom f1 = dom F and
A13: for x being set st x in dom F holds
for C being Category st C = F . x holds
f1 . x = the carrier' of C and
A14: dom f2 = dom F and
A15: for x being set st x in dom F holds
for C being Category st C = F . x holds
f2 . x = the carrier' of C ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom F implies f1 . x = f2 . x )
assume A16: x in dom F ; ::_thesis: f1 . x = f2 . x
then reconsider C = F . x as Category by Def1;
thus f1 . x = the carrier' of C by A13, A16
.= f2 . x by A15, A16 ; ::_thesis: verum
end;
hence  f1 = f2 by A12, A14, FUNCT_1:2; ::_thesis: verum
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 carrier 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 carrier' of C ) ) );

registration
let A be non empty set ;
let F be ManySortedCategory of A;
cluster Objs F ->  non-empty A -defined ;
coherence
 Objs F is A -defined
proof
dom (Objs F) = dom F by Def2
.= A by PARTFUN1:def_2 ;
hence  Objs F is A -defined by RELAT_1:def_18; ::_thesis: verum
end;
cluster Mphs F ->  non-empty A -defined ;
coherence
 Mphs F is A -defined
proof
dom (Mphs F) = dom F by Def3
.= A by PARTFUN1:def_2 ;
hence  Mphs F is A -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
let F be ManySortedCategory of A;
cluster Objs F ->  non-empty total ;
coherence
 Objs F is total
proof
dom (Objs F) = dom F by Def2
.= A by PARTFUN1:def_2 ;
hence  Objs F is total by PARTFUN1:def_2; ::_thesis: verum
end;
cluster Mphs F ->  non-empty total ;
coherence
 Mphs F is total
proof
dom (Mphs F) = dom F by Def3
.= A by PARTFUN1:def_2 ;
hence  Mphs F is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;

theorem :: INDEX_1:3
for X being set
for C being Category holds
( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )
proof
let X be set ; ::_thesis: for C being Category holds
( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )
let C be Category; ::_thesis: ( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )
A1: dom (X --> C) = X by FUNCOP_1:13;
A2: dom (Objs (X --> C)) = dom (X --> C) by Def2;
now__::_thesis:_for_a_being_set_st_a_in_dom_(Objs_(X_-->_C))_holds_
(Objs_(X_-->_C))_._a_=_the_carrier_of_C
let a be set ; ::_thesis: ( a in dom (Objs (X --> C)) implies (Objs (X --> C)) . a = the carrier of C )
assume A3: a in dom (Objs (X --> C)) ; ::_thesis: (Objs (X --> C)) . a = the carrier of C
then  (X --> C) . a = C by A2, A1, FUNCOP_1:7;
hence  (Objs (X --> C)) . a = the carrier of C by A2, A3, Def2; ::_thesis: verum
end;
hence  Objs (X --> C) = X --> the carrier of C by A2, A1, FUNCOP_1:11; ::_thesis: Mphs (X --> C) = X --> the carrier' of C
A4: dom (Mphs (X --> C)) = dom (X --> C) by Def3;
now__::_thesis:_for_a_being_set_st_a_in_dom_(Mphs_(X_-->_C))_holds_
(Mphs_(X_-->_C))_._a_=_the_carrier'_of_C
let a be set ; ::_thesis: ( a in dom (Mphs (X --> C)) implies (Mphs (X --> C)) . a = the carrier' of C )
assume A5: a in dom (Mphs (X --> C)) ; ::_thesis: (Mphs (X --> C)) . a = the carrier' of C
then  (X --> C) . a = C by A4, A1, FUNCOP_1:7;
hence  (Mphs (X --> C)) . a = the carrier' of C by A4, A5, Def3; ::_thesis: verum
end;
hence  Mphs (X --> C) = X --> the carrier' of C by A4, A1, FUNCOP_1:11; ::_thesis: verum
end;

begin

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
set f = the ManySortedSet of A;
set g = the ManySortedSet of B;
take  [ the ManySortedSet of A, the ManySortedSet of B] ; ::_thesis: ex f being ManySortedSet of A ex g being ManySortedSet of B st [ the ManySortedSet of A, the ManySortedSet of B] = [f,g]
take  the ManySortedSet of A ; ::_thesis: ex g being ManySortedSet of B st [ the ManySortedSet of A, the ManySortedSet of B] = [ the ManySortedSet of A,g]
take  the ManySortedSet of B ; ::_thesis: [ the ManySortedSet of A, the ManySortedSet of B] = [ the ManySortedSet of A, the ManySortedSet of B]
thus  [ the ManySortedSet of A, the ManySortedSet of B] = [ the ManySortedSet of A, the ManySortedSet of B] ; ::_thesis: verum
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
take  f ; :: according to INDEX_1:def_4 ::_thesis: ex g being ManySortedSet of B st [f,g] = [f,g]
take  g ; ::_thesis: [f,g] = [f,g]
thus  [f,g] = [f,g] ; ::_thesis: verum
end;
end;

registration
let A, B be set ;
let X be ManySortedSet of A,B;
clusterX `1  ->  Relation-like Function-like ;
coherence
 ( X `1 is Function-like & X `1 is Relation-like )
proof
 ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence  ( X `1 is Function-like & X `1 is Relation-like ) by MCART_1:7; ::_thesis: verum
end;
clusterX `2  ->  Relation-like Function-like ;
coherence
 ( X `2 is Function-like & X `2 is Relation-like )
proof
 ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence  ( X `2 is Function-like & X `2 is Relation-like ) by MCART_1:7; ::_thesis: verum
end;
end;

registration
let A, B be set ;
let X be ManySortedSet of A,B;
clusterX `1  -> A -defined ;
coherence
 X `1 is A -defined
proof
 ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence  X `1 is A -defined by MCART_1:7; ::_thesis: verum
end;
clusterX `2  -> B -defined ;
coherence
 X `2 is B -defined
proof
 ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence  X `2 is B -defined by MCART_1:7; ::_thesis: verum
end;
end;

registration
let A, B be set ;
let X be ManySortedSet of A,B;
clusterX `1  -> A -defined total for A -defined Function;
coherence
 for b1 being A -defined Function st b1 = X `1 holds
b1 is total
proof
 ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence  for b1 being A -defined Function st b1 = X `1 holds
b1 is total by MCART_1:7; ::_thesis: verum
end;
clusterX `2  -> B -defined total for B -defined Function;
coherence
 for b1 being B -defined Function st b1 = X `2 holds
b1 is total
proof
 ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence  for b1 being B -defined Function st b1 = X `2 holds
b1 is total by MCART_1:7; ::_thesis: verum
end;
end;

definition
let A, B be set ;
let IT be ManySortedSet of A,B;
attrIT is Category-yielding_on_first  means :Def5: :: INDEX_1:def 5
IT `1 is Category-yielding ;
attrIT 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 for 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
set g = the ManySortedFunction of B;
set f = the ManySortedCategory of A;
reconsider X = [ the ManySortedCategory of A, the ManySortedFunction of B] as ManySortedSet of A,B ;
take  X ; ::_thesis: ( X is Category-yielding_on_first & X is Function-yielding_on_second )
thus  ( X `1 is Category-yielding & X `2 is Function-yielding ) by MCART_1:7; :: according to INDEX_1:def_5,INDEX_1:def_6 ::_thesis: verum
end;
end;

registration
let A, B be set ;
let X be Category-yielding_on_first ManySortedSet of A,B;
clusterX `1  ->  Category-yielding ;
coherence
 X `1 is Category-yielding by Def5;
end;

registration
let A, B be set ;
let X be Function-yielding_on_second ManySortedSet of A,B;
clusterX `2  ->  Function-yielding ;
coherence
 X `2 is Function-yielding by Def6;
end;

registration
let f be Function-yielding Function;
cluster proj2 f ->  functional ;
coherence
 rng f is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in rng f or x is set )
assume  x in rng f ; ::_thesis: x is set
then  ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def_3;
hence  x is set ; ::_thesis: verum
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
 ( [f,g] `1 = f & [f,g] `2 = g ) ;
hence  [f,g] is Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B by Def5, Def6; ::_thesis: verum
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
defpred S1[ set , set ] means  ex a9 being Element of A ex t being Functor of F . a9,G . a9 st
( $1 = a9 & $2 = t );
A1: now__::_thesis:_for_a_being_set_st_a_in_A_holds_
ex_f9_being_set_st_S1[a,f9]
let a be set ; ::_thesis: ( a in A implies ex f9 being set st S1[a,f9] )
assume  a in A ; ::_thesis: ex f9 being set st S1[a,f9]
then reconsider a9 = a as Element of A ;
set f = the Functor of F . a9,G . a9;
reconsider f9 = the Functor of F . a9,G . a9 as set ;
take f9 = f9; ::_thesis: S1[a,f9]
thus  S1[a,f9] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = A & ( for a being set st a in A holds
S1[a,f . a] ) ) from CLASSES1:sch_1(A1);
 f is Function-yielding
proof
let a be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not a in proj1 f or f . a is set )
assume  a in dom f ; ::_thesis: f . a is set
then  ex a9 being Element of A ex t being Functor of F . a9,G . a9 st
( a = a9 & f . a = t ) by A2;
hence  f . a is set ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of A by A2, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for a being Element of A holds f . a is Functor of F . a,G . a
let a be Element of A; ::_thesis: f . a is Functor of F . a,G . a
 ex a9 being Element of A ex t being Functor of F . a9,G . a9 st
( a = a9 & f . a = t ) by A2;
hence  f . a is Functor of F . a,G . a ; ::_thesis: verum
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
consider f being ManySortedSet of F1() such that
A2: for a being set st a in F1() holds
f . a = F4(a) from PBOOLE:sch_4();
 f is Function-yielding
proof
let a be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not a in proj1 f or f . a is set )
assume  a in dom f ; ::_thesis: f . a is set
then reconsider a = a as Element of F1() by PARTFUN1:def_2;
 f . a = F4(a) by A2;
hence  f . a is set by A1; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of F1() ;
 f is ManySortedFunctor of F2(),F3()
proof
let a be Element of F1(); :: according to INDEX_1:def_7 ::_thesis: f . a is Functor of F2() . a,F3() . a
 f . a = F4(a) by A2;
hence  f . a is Functor of F2() . a,F3() . a by A1; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunctor of F2(),F3() ;
take  f ; ::_thesis: for a being Element of F1() holds f . a = F4(a)
thus  for a being Element of F1() holds f . a = F4(a) by A2; ::_thesis: verum
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 funcf . a ->  Functor of F . a,G . a;
coherence
 f . a is Functor of F . a,G . a by Def7;
end;

begin

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
set g = the ManySortedCategory of A;
set f = the ManySortedFunctor of the ManySortedCategory of A * F, the ManySortedCategory of A * G;
take I = [ the ManySortedCategory of A, the ManySortedFunctor of the ManySortedCategory of A * F, the ManySortedCategory of A * G]; ::_thesis: I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G
 I `1 = the ManySortedCategory of A by MCART_1:7;
hence  I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G by MCART_1:7; ::_thesis: verum
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
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
let A, B be non empty set ; ::_thesis: 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)
let F, G be Function of B,A; ::_thesis: 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)
let I be Indexing of F,G; ::_thesis: for m being Element of B holds (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)
reconsider H = I `2 as ManySortedFunctor of (I `1) * F,(I `1) * G by Def8;
let m be Element of B; ::_thesis: (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)
 dom ((I `1) * F) = B by PARTFUN1:def_2;
then A1: ((I `1) * F) . m = (I `1) . (F . m) by FUNCT_1:12;
 ( H . m is Functor of ((I `1) * F) . m,((I `1) * G) . m & dom ((I `1) * G) = B ) by PARTFUN1:def_2;
hence  (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m) by A1, FUNCT_1:12; ::_thesis: verum
end;

theorem :: INDEX_1:5
for C being Category
for I being Indexing of the Source of C, the Target of C
for m being Morphism of C holds (I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m) by Th4;

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 funcI `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__::_thesis:_for_A,_B_being_non_empty_set_
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 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 ) )
consider C being strict Categorial full Category such that
A1: the carrier 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 ) )
A2: dom (I `1) = A by PARTFUN1:def_2;
hence  for a being Element of A holds (I `1) . a is Object of C by A1, FUNCT_1:def_3; ::_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
A3: (I `2) . b is Functor of (I `1) . (F . b),(I `1) . (G . b) by Th4;
 ( (I `1) . (F . b) is Object of C & (I `1) . (G . b) is Object of C ) by A2, A1, FUNCT_1:def_3;
hence  [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C by A3, 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
 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 ) ) by Lm1;
hence  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 ) ) ; ::_thesis: verum
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 non empty non void V52() strict Category-like V65() V66() V67() with_identities with_triple-like_morphisms Categorial full for TargetCat of I;
existence
 ex b1 being TargetCat of I st
( b1 is full & b1 is strict )
proof
consider C being strict Categorial full Category such that
A1: ( ( 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 ) ) by Lm1;
 C is TargetCat of I by A1, Def9;
hence  ex b1 being TargetCat of I st
( b1 is full & b1 is strict ) ; ::_thesis: verum
end;
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 #) ;
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
set I2 = B --> (id C);
set I1 = A --> C;
A2: [(A --> C),(B --> (id C))] `1 = A --> C ;
A3: [(A --> C),(B --> (id C))] `2 = B --> (id C) ;
 B --> (id C) is ManySortedFunctor of (A --> C) * F,(A --> C) * G
proof
let a be Element of B; :: according to INDEX_1:def_7 ::_thesis: (B --> (id C)) . a is Functor of ((A --> C) * F) . a,((A --> C) * G) . a
 ( (A --> C) . (F . a) = C & dom ((A --> C) * F) = B ) by FUNCOP_1:7, PARTFUN1:def_2;
then A4: ( (B --> (id C)) . a = id C & ((A --> C) * F) . a = C ) by FUNCOP_1:7, FUNCT_1:12;
 ( (A --> C) . (G . a) = C & dom ((A --> C) * G) = B ) by FUNCOP_1:7, PARTFUN1:def_2;
hence  (B --> (id C)) . a is Functor of ((A --> C) * F) . a,((A --> C) * G) . a by A4, FUNCT_1:12; ::_thesis: verum
end;
then reconsider I = [(A --> C),(B --> (id C))] as Indexing of F,G by A2, A3, Def8;
take  I ; ::_thesis: ( ( for a being Element of A holds (I `2) . (i . a) = id ((I `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) ) )
hereby  ::_thesis: for m1, m2 being Element of B st F . m2 = G . m1 holds
(I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
let a be Element of A; ::_thesis: (I `2) . (i . a) = id ((I `1) . a)
thus (I `2) . (i . a) = id C by A3, FUNCOP_1:7
.= id ((I `1) . a) by A2, FUNCOP_1:7 ; ::_thesis: verum
end;
let m1, m2 be Element of B; ::_thesis: ( F . m2 = G . m1 implies (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) )
reconsider mm1 = m1, mm2 = m2 as Morphism of C by A1;
assume  F . m2 = G . m1 ; ::_thesis: (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
then  cod mm1 = dom mm2 by A1;
then  [m2,m1] in dom c by A1, CAT_1:def_6;
then A5: (I `2) . (c . [m2,m1]) = id C by A3, FUNCOP_1:7, PARTFUN1:4;
 ( (I `2) . m1 = id C & (I `2) . m2 = id C ) by A3, FUNCOP_1:7;
hence  (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) by A5, FUNCT_2:17; ::_thesis: verum
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 #) 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 Source of C, the Target of C, the Comp of C, IdMap C;
mode coIndexing of C is Indexing of the Target of C, the Source of C, ~ the Comp of C, IdMap C;
end;

theorem Th6: :: INDEX_1:6
for C being Category
for I being Indexing of the Source of C, the Target 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
let C be Category; ::_thesis: for I being Indexing of the Source of C, the Target 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) ) ) )
reconsider D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) as Category by CAT_5:1;
let I be Indexing of the Source of C, the Target of C; ::_thesis: ( 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) ) ) )
A1: D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) ;
hereby  ::_thesis: ( ( 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) ) implies I is Indexing of C )
assume A2: I is Indexing of C ; ::_thesis: ( ( 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) ) )
thus  for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ::_thesis: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)
proof
let a be Object of C; ::_thesis: (I `2) . (id a) = id ((I `1) . a)
 id a = (IdMap C) . a by ISOCAT_1:def_12;
hence  (I `2) . (id a) = id ((I `1) . a) by A1, Def10, A2; ::_thesis: verum
end;
let m1, m2 be Morphism of C; ::_thesis: ( dom m2 = cod m1 implies (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) )
assume A3: dom m2 = cod m1 ; ::_thesis: (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)
then  (I `2) . ( the Comp of C . (m2,m1)) = ((I `2) . m2) * ((I `2) . m1) by A1, A2, Def10;
hence  (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) by A3, CAT_1:16; ::_thesis: verum
end;
assume that
A4: for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) and
A5: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) ; ::_thesis: I is Indexing of C
thus  ex D being Category st D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) by A1; :: according to INDEX_1:def_10 ::_thesis: ( ( for a being Element of the carrier of C holds (I `2) . ((IdMap C) . a) = id ((I `1) . a) ) & ( for m1, m2 being Element of the carrier' of C st the Source of C . m2 = the Target of C . m1 holds
(I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) ) )
hereby  ::_thesis: for m1, m2 being Element of the carrier' of C st the Source of C . m2 = the Target of C . m1 holds
(I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
let a be Object of C; ::_thesis: (I `2) . ((IdMap C) . a) = id ((I `1) . a)
 id a = (IdMap C) . a by ISOCAT_1:def_12;
hence (I `2) . ((IdMap C) . a) = (I `2) . (id a)
.= id ((I `1) . a) by A4 ;
::_thesis: verum
end;
let m1, m2 be Morphism of C; ::_thesis: ( the Source of C . m2 = the Target of C . m1 implies (I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) )
assume  the Source of C . m2 = the Target of C . m1 ; ::_thesis: (I `2) . ( the Comp of C . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
then A6: dom m2 = cod m1 ;
then A7: (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) by A5;
thus (I `2) . ( the Comp of C . [m2,m1]) = (I `2) . ( the Comp of C . (m2,m1))
.= ((I `2) . m2) * ((I `2) . m1) by A6, A7, CAT_1:16 ; ::_thesis: verum
end;

theorem Th7: :: INDEX_1:7
for C being Category
for I being Indexing of the Target of C, the Source 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
let C be Category; ::_thesis: for I being Indexing of the Target of C, the Source 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) ) ) )
let I be Indexing of the Target of C, the Source of C; ::_thesis: ( 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) ) ) )
A1: C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) ;
hereby  ::_thesis: ( ( 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) ) implies I is coIndexing of C )
assume A2: I is coIndexing of C ; ::_thesis: ( ( 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) ) )
thus  for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ::_thesis: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2)
proof
let a be Object of C; ::_thesis: (I `2) . (id a) = id ((I `1) . a)
 id a = (IdMap C) . a by ISOCAT_1:def_12;
hence  (I `2) . (id a) = id ((I `1) . a) by A1, Def10, A2; ::_thesis: verum
end;
let m1, m2 be Morphism of C; ::_thesis: ( dom m2 = cod m1 implies (I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2) )
assume A3: dom m2 = cod m1 ; ::_thesis: (I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2)
then A4: [m2,m1] in dom the Comp of C by CAT_1:15;
 (I `2) . ((~ the Comp of C) . (m1,m2)) = ((I `2) . m1) * ((I `2) . m2) by A1, A2, A3, Def10;
then  (I `2) . ( the Comp of C . (m2,m1)) = ((I `2) . m1) * ((I `2) . m2) by A4, FUNCT_4:def_2;
hence  (I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2) by A3, CAT_1:16; ::_thesis: verum
end;
assume that
A5: for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) and
A6: for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2) ; ::_thesis: I is coIndexing of C
thus  ex D being Category st D = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) by A1; :: according to INDEX_1:def_10 ::_thesis: ( ( for a being Element of the carrier of C holds (I `2) . ((IdMap C) . a) = id ((I `1) . a) ) & ( for m1, m2 being Element of the carrier' of C st the Target of C . m2 = the Source of C . m1 holds
(I `2) . ((~ the Comp of C) . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) ) )
hereby  ::_thesis: for m1, m2 being Element of the carrier' of C st the Target of C . m2 = the Source of C . m1 holds
(I `2) . ((~ the Comp of C) . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
let a be Object of C; ::_thesis: (I `2) . ((IdMap C) . a) = id ((I `1) . a)
 id a = (IdMap C) . a by ISOCAT_1:def_12;
hence (I `2) . ((IdMap C) . a) = (I `2) . (id a)
.= id ((I `1) . a) by A5 ;
::_thesis: verum
end;
let m1, m2 be Morphism of C; ::_thesis: ( the Target of C . m2 = the Source of C . m1 implies (I `2) . ((~ the Comp of C) . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) )
assume  the Target of C . m2 = the Source of C . m1 ; ::_thesis: (I `2) . ((~ the Comp of C) . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
then A7: dom m1 = cod m2 ;
then  (I `2) . (m1 (*) m2) = ((I `2) . m2) * ((I `2) . m1) by A6;
then A8: (I `2) . ( the Comp of C . (m1,m2)) = ((I `2) . m2) * ((I `2) . m1) by A7, CAT_1:16;
A9: [m1,m2] in dom the Comp of C by A7, CAT_1:15;
thus (I `2) . ((~ the Comp of C) . [m2,m1]) = (I `2) . ((~ the Comp of C) . (m2,m1))
.= ((I `2) . m2) * ((I `2) . m1) by A8, A9, FUNCT_4:def_2 ; ::_thesis: verum
end;

Lm2:  for C being Category holds IdMap C = IdMap (C opp)
proof
let C be Category; ::_thesis: IdMap C = IdMap (C opp)
thus  the carrier of C = the carrier of (C opp) ; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier of C holds (IdMap C) . b1 = (IdMap (C opp)) . b1
let o be Element of the carrier of C; ::_thesis: (IdMap C) . o = (IdMap (C opp)) . o
thus (IdMap C) . o = id o by ISOCAT_1:def_12
.= id (o opp) by OPPCAT_1:71
.= (IdMap (C opp)) . (o opp) by ISOCAT_1:def_12
.= (IdMap (C opp)) . o ; ::_thesis: verum
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
let C be Category; ::_thesis: for x being set holds
( x is coIndexing of C iff x is Indexing of (C opp) )
let x be set ; ::_thesis: ( x is coIndexing of C iff x is Indexing of (C opp) )
A1: IdMap C = IdMap (C opp) by Lm2;
thus  ( x is coIndexing of C iff x is Indexing of (C opp) ) by A1; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let I be Indexing of C; ::_thesis: 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
let c1, c2 be Object of C; ::_thesis: ( not Hom (c1,c2) is empty implies for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c1,(I `1) . c2 )
assume A1: not Hom (c1,c2) is empty ; ::_thesis: for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c1,(I `1) . c2
let m be Morphism of c1,c2; ::_thesis: (I `2) . m is Functor of (I `1) . c1,(I `1) . c2
 dom ((I `1) * the Source of C) = the carrier' of C by PARTFUN1:def_2;
then A2: ( dom ((I `1) * the Target of C) = the carrier' of C & ((I `1) * the Source of C) . m = (I `1) . ( the Source of C . m) ) by FUNCT_1:12, PARTFUN1:def_2;
 ( dom m = c1 & cod m = c2 ) by A1, CAT_1:5;
hence  (I `2) . m is Functor of (I `1) . c1,(I `1) . c2 by A2, FUNCT_1:12; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let I be coIndexing of C; ::_thesis: 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
let c1, c2 be Object of C; ::_thesis: ( not Hom (c1,c2) is empty implies for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c2,(I `1) . c1 )
assume A1: not Hom (c1,c2) is empty ; ::_thesis: for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c2,(I `1) . c1
let m be Morphism of c1,c2; ::_thesis: (I `2) . m is Functor of (I `1) . c2,(I `1) . c1
 dom ((I `1) * the Source of C) = the carrier' of C by PARTFUN1:def_2;
then A2: ( dom ((I `1) * the Target of C) = the carrier' of C & ((I `1) * the Source of C) . m = (I `1) . ( the Source of C . m) ) by FUNCT_1:12, PARTFUN1:def_2;
 ( dom m = c1 & cod m = c2 ) by A1, CAT_1:5;
hence  (I `2) . m is Functor of (I `1) . c2,(I `1) . c1 by A2, FUNCT_1:12; ::_thesis: verum
end;

definition
let C be Category;
let I be Indexing of C;
let T be TargetCat of I;
funcI -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
A1: rng (I `1) c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (I `1) or x in the carrier of T )
assume  x in rng (I `1) ; ::_thesis: x in the carrier of T
then consider a being set  such that
A2: a in dom (I `1) and
A3: x = (I `1) . a by FUNCT_1:def_3;
reconsider a = a as Object of C by A2, PARTFUN1:def_2;
 (I `1) . a is Object of T by Def9;
hence  x in the carrier of T by A3; ::_thesis: verum
end;
 dom (I `1) = the carrier of C by PARTFUN1:def_2;
then reconsider I1 = I `1 as Function of the carrier of C, the carrier of T by A1, FUNCT_2:def_1, RELSET_1:4;
deffunc H1( Object of C) ->  Element of the carrier of T = I1 . $1;
deffunc H2( Morphism of C) ->  set = [[((I `1) . (dom $1)),((I `1) . (cod $1))],((I `2) . $1)];
A4: now__::_thesis:_for_f_being_Morphism_of_C_holds_
(_H2(f)_is_Morphism_of_T_&_(_for_g_being_Morphism_of_T_st_g_=_H2(f)_holds_
(_dom_g_=_H1(_dom_f)_&_cod_g_=_H1(_cod_f)_)_)_)
let f be Morphism of C; ::_thesis: ( H2(f) is Morphism of T & ( for g being Morphism of T st g = H2(f) holds
( dom g = H1( dom f) & cod g = H1( cod f) ) ) )
thus  H2(f) is Morphism of T by Def9; ::_thesis: for g being Morphism of T st g = H2(f) holds
( dom g = H1( dom f) & cod g = H1( cod f) )
let g be Morphism of T; ::_thesis: ( g = H2(f) implies ( dom g = H1( dom f) & cod g = H1( cod f) ) )
assume A5: g = H2(f) ; ::_thesis: ( dom g = H1( dom f) & cod g = H1( cod f) )
hence  dom g = H2(f) `11 by CAT_5:13
.= H1( dom f) by MCART_1:85 ;
::_thesis: cod g = H1( cod f)
thus  cod g = H2(f) `12 by A5, CAT_5:13
.= H1( cod f) by MCART_1:85 ; ::_thesis: verum
end;
A6: now__::_thesis:_for_f1,_f2_being_Morphism_of_C
for_g1,_g2_being_Morphism_of_T_st_g1_=_H2(f1)_&_g2_=_H2(f2)_&_dom_f2_=_cod_f1_holds_
H2(f2_(*)_f1)_=_g2_(*)_g1
let f1, f2 be Morphism of C; ::_thesis: for g1, g2 being Morphism of T st g1 = H2(f1) & g2 = H2(f2) & dom f2 = cod f1 holds
H2(f2 (*) f1) = g2 (*) g1
let g1, g2 be Morphism of T; ::_thesis: ( g1 = H2(f1) & g2 = H2(f2) & dom f2 = cod f1 implies H2(f2 (*) f1) = g2 (*) g1 )
assume that
A7: ( g1 = H2(f1) & g2 = H2(f2) ) and
A8: dom f2 = cod f1 ; ::_thesis: H2(f2 (*) f1) = g2 (*) g1
A9: ( dom (f2 (*) f1) = dom f1 & cod (f2 (*) f1) = cod f2 ) by A8, CAT_1:17;
A10: ( (I `2) . f1 is Functor of (I `1) . (dom f1),(I `1) . (cod f1) & (I `2) . f2 is Functor of (I `1) . (dom f2),(I `1) . (cod f2) ) by Th4;
 (I `2) . (f2 (*) f1) = ((I `2) . f2) * ((I `2) . f1) by A8, Th6;
hence  H2(f2 (*) f1) = g2 (*) g1 by A7, A8, A10, A9, CAT_5:def_6; ::_thesis: verum
end;
A11: now__::_thesis:_for_a_being_Object_of_C_holds_H2(_id_a)_=_id_H1(a)
let a be Object of C; ::_thesis: H2( id a) = id H1(a)
thus H2( id a) = [[(I1 . a),(I1 . a)],(id ((I `1) . a))] by Th6
.= id H1(a) by CAT_5:def_6 ; ::_thesis: verum
end;
thus  ex F being Functor of C,T st
for f being Morphism of C holds F . f = H2(f) from CAT_5:sch_3(A4, A11, A6); ::_thesis: verum
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
let F1, F2 be Functor of C,T; ::_thesis: ( ( for f being Morphism of C holds F1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) & ( for f being Morphism of C holds F2 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) implies F1 = F2 )
assume that
A12: for f being Morphism of C holds F1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] and
A13: for f being Morphism of C holds F2 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Morphism_of_C_holds_F1_._f_=_F2_._f
let f be Morphism of C; ::_thesis: F1 . f = F2 . f
thus F1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] by A12
.= F2 . f by A13 ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
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
let C be Category; ::_thesis: for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1
let I be Indexing of C; ::_thesis: for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1
let T be TargetCat of I; ::_thesis: Obj (I -functor (C,T)) = I `1
A1: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_C_holds_
(Obj_(I_-functor_(C,T)))_._x_=_(I_`1)_._x
let x be set ; ::_thesis: ( x in the carrier of C implies (Obj (I -functor (C,T))) . x = (I `1) . x )
assume  x in the carrier of C ; ::_thesis: (Obj (I -functor (C,T))) . x = (I `1) . x
then reconsider a = x as Object of C ;
A2: ( dom (id a) = a & cod (id a) = a ) ;
(Obj (I -functor (C,T))) . a = dom (id ((Obj (I -functor (C,T))) . a))
.= dom ((I -functor (C,T)) . (id a)) by CAT_1:68
.= ((I -functor (C,T)) . (id a)) `11 by CAT_5:2
.= [[((I `1) . a),((I `1) . a)],((I `2) . (id a))] `11 by A2, Def11 ;
hence  (Obj (I -functor (C,T))) . x = (I `1) . x by MCART_1:85; ::_thesis: verum
end;
 ( dom (Obj (I -functor (C,T))) = the carrier of C & dom (I `1) = the carrier of C ) by FUNCT_2:def_1, PARTFUN1:def_2;
hence  Obj (I -functor (C,T)) = I `1 by A1, FUNCT_1:2; ::_thesis: verum
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
let C be Category; ::_thesis: 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)) )
let I be Indexing of C; ::_thesis: 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)) )
let T1, T2 be TargetCat of I; ::_thesis: ( I -functor (C,T1) = I -functor (C,T2) & Obj (I -functor (C,T1)) = Obj (I -functor (C,T2)) )
A1: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C_holds_
(I_-functor_(C,T1))_._x_=_(I_-functor_(C,T2))_._x
let x be set ; ::_thesis: ( x in the carrier' of C implies (I -functor (C,T1)) . x = (I -functor (C,T2)) . x )
assume  x in the carrier' of C ; ::_thesis: (I -functor (C,T1)) . x = (I -functor (C,T2)) . x
then reconsider f = x as Morphism of C ;
thus (I -functor (C,T1)) . x = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] by Def11
.= (I -functor (C,T2)) . x by Def11 ; ::_thesis: verum
end;
 ( dom (I -functor (C,T1)) = the carrier' of C & dom (I -functor (C,T2)) = the carrier' of C ) by FUNCT_2:def_1;
hence  I -functor (C,T1) = I -functor (C,T2) by A1, FUNCT_1:2; ::_thesis: Obj (I -functor (C,T1)) = Obj (I -functor (C,T2))
A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_C_holds_
(Obj_(I_-functor_(C,T1)))_._x_=_(Obj_(I_-functor_(C,T2)))_._x
let x be set ; ::_thesis: ( x in the carrier of C implies (Obj (I -functor (C,T1))) . x = (Obj (I -functor (C,T2))) . x )
assume  x in the carrier of C ; ::_thesis: (Obj (I -functor (C,T1))) . x = (Obj (I -functor (C,T2))) . x
then reconsider a = x as Object of C ;
thus (Obj (I -functor (C,T1))) . x = (I `1) . a by Lm3
.= (Obj (I -functor (C,T2))) . x by Lm3 ; ::_thesis: verum
end;
 ( dom (Obj (I -functor (C,T1))) = the carrier of C & dom (Obj (I -functor (C,T2))) = the carrier of C ) by FUNCT_2:def_1;
hence  Obj (I -functor (C,T1)) = Obj (I -functor (C,T2)) by A2, FUNCT_1:2; ::_thesis: verum
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 by Lm3;

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
set T = the TargetCat of I;
let T1, T2 be strict TargetCat of I; ::_thesis: ( ( for T being TargetCat of I holds T1 = Image (I -functor (C,T)) ) & ( for T being TargetCat of I holds T2 = Image (I -functor (C,T)) ) implies T1 = T2 )
assume that
A1: for T being TargetCat of I holds T1 = Image (I -functor (C,T)) and
A2: for T being TargetCat of I holds T2 = Image (I -functor (C,T)) ; ::_thesis: T1 = T2
thus T1 = Image (I -functor (C, the TargetCat of I)) by A1
.= T2 by A2 ; ::_thesis: verum
end;
existence
 ex b1 being strict TargetCat of I st
for T being TargetCat of I holds b1 = Image (I -functor (C,T))
proof
set S = the TargetCat of I;
reconsider T = Image (I -functor (C, the TargetCat of I)) as strict Subcategory of the TargetCat of I ;
reconsider F = I -functor (C, the TargetCat of I) as Functor of C,T by CAT_5:8;
 T is TargetCat of I
proof
 the carrier of T = rng (Obj (I -functor (C, the TargetCat of I))) by CAT_5:def_3;
then A3: the carrier of T = rng (I `1) by Lm3;
 dom (I `1) = the carrier of C by PARTFUN1:def_2;
hence  for a being Object of C holds (I `1) . a is Object of T by A3, FUNCT_1:def_3; :: according to INDEX_1:def_9 ::_thesis: for b being Element of the carrier' of C holds [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of T
let b be Morphism of C; ::_thesis: [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of T
 F . b = [[((I `1) . (dom b)),((I `1) . (cod b))],((I `2) . b)] by Def11;
hence  [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of T ; ::_thesis: verum
end;
then reconsider T = T as strict TargetCat of I ;
take  T ; ::_thesis: for T being TargetCat of I holds T = Image (I -functor (C,T))
let T9 be TargetCat of I; ::_thesis: T = Image (I -functor (C,T9))
thus  T = Image (I -functor (C,T9)) by Th11, CAT_5:22; ::_thesis: verum
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
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
let C be Category; ::_thesis: for I being Indexing of C
for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )
let I be Indexing of C; ::_thesis: for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )
let D be Categorial Category; ::_thesis: ( rng I is Subcategory of D iff D is TargetCat of I )
hereby  ::_thesis: ( D is TargetCat of I implies rng I is Subcategory of D )
assume A1: rng I is Subcategory of D ; ::_thesis: D is TargetCat of I
thus  D is TargetCat of I ::_thesis: verum
proof
hereby  :: according to INDEX_1:def_9 ::_thesis: for b being Element of the carrier' of C holds [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of D
let a be Object of C; ::_thesis: (I `1) . a is Object of D
 (I `1) . a is Object of (rng I) by Def9;
hence  (I `1) . a is Object of D by A1, CAT_2:6; ::_thesis: verum
end;
let b be Morphism of C; ::_thesis: [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of D
 [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of (rng I) by Def9;
hence  [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of D by A1, CAT_2:8; ::_thesis: verum
end;
end;
assume  D is TargetCat of I ; ::_thesis: rng I is Subcategory of D
then reconsider T = D as TargetCat of I ;
 rng I = Image (I -functor (C,T)) by Def12;
hence  rng I is Subcategory of D ; ::_thesis: verum
end;

definition
let C be Category;
let I be Indexing of C;
let m be Morphism of C;
funcI . 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
 dom ((I `1) * the Source of C) = the carrier' of C by PARTFUN1:def_2;
then  ( dom ((I `1) * the Target of C) = the carrier' of C & ((I `1) * the Source of C) . m = (I `1) . ( the Source of C . m) ) by FUNCT_1:12, PARTFUN1:def_2;
hence  (I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m) by FUNCT_1:12; ::_thesis: verum
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;
funcI . 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
 dom ((I `1) * the Source of C) = the carrier' of C by PARTFUN1:def_2;
then  ( dom ((I `1) * the Target of C) = the carrier' of C & ((I `1) * the Source of C) . m = (I `1) . ( the Source of C . m) ) by FUNCT_1:12, PARTFUN1:def_2;
hence  (I `2) . m is Functor of (I `1) . (cod m),(I `1) . (dom m) by FUNCT_1:12; ::_thesis: verum
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__::_thesis:_for_C,_D_being_Category
for_m_being_Morphism_of_C_holds_([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`2)_._m_is_Functor_of_(([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`1)_*_the_Source_of_C)_._m,(([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`1)_*_the_Target_of_C)_._m
let C, D be Category; ::_thesis: for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m
set F = the carrier of C --> D;
set G = the carrier' of C --> (id D);
set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];
let m be Morphism of C; ::_thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m
 dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def_2;
then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:12
.= ( the carrier of C --> D) . ( the Source of C . m)
.= D by FUNCOP_1:7 ;
 dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def_2;
then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:12
.= ( the carrier of C --> D) . ( the Target of C . m)
.= D by FUNCOP_1:7 ;
([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m
.= id D by FUNCOP_1:7 ;
hence  ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m by A1, A2; ::_thesis: verum
end;

Lm5: now__::_thesis:_for_C,_D_being_Category
for_m_being_Morphism_of_C_holds_([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`2)_._m_is_Functor_of_(([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`1)_*_the_Target_of_C)_._m,(([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`1)_*_the_Source_of_C)_._m
let C, D be Category; ::_thesis: for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m
set F = the carrier of C --> D;
set G = the carrier' of C --> (id D);
set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];
let m be Morphism of C; ::_thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m
 dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def_2;
then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:12
.= ( the carrier of C --> D) . ( the Source of C . m)
.= D by FUNCOP_1:7 ;
 dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def_2;
then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:12
.= ( the carrier of C --> D) . ( the Target of C . m)
.= D by FUNCOP_1:7 ;
([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m
.= id D by FUNCOP_1:7 ;
hence  ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m by A1, A2; ::_thesis: verum
end;

theorem :: INDEX_1:15
for C, D being Category holds
( [( the carrier of C --> D),( the carrier' of C --> (id D))] is Indexing of C & [( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C )
proof
let C, D be Category; ::_thesis: ( [( the carrier of C --> D),( the carrier' of C --> (id D))] is Indexing of C & [( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C )
set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];
set I = [( the carrier of C --> D),( the carrier' of C --> (id D))];
A1: [( the carrier of C --> D),( the carrier' of C --> (id D))] `2 = the carrier' of C --> (id D) ;
A2: now__::_thesis:_for_a_being_Object_of_C_holds_([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`2)_._(id_a)_=_id_(([(_the_carrier_of_C_-->_D),(_the_carrier'_of_C_-->_(id_D))]_`1)_._a)
let a be Object of C; ::_thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . (id a) = id (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . a)
thus ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . (id a) = id D by FUNCOP_1:7
.= id (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . a) by FUNCOP_1:7 ; ::_thesis: verum
end;
 for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m by Lm4;
then  [( the carrier of C --> D),( the carrier' of C --> (id D))] `2 is ManySortedFunctor of ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C,([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C by Def7;
then reconsider H = [( the carrier of C --> D),( the carrier' of C --> (id D))] as Indexing of the Source of C, the Target of C by Def8;
now__::_thesis:_for_m1,_m2_being_Morphism_of_C_st_dom_m2_=_cod_m1_holds_
(H_`2)_._(m2_(*)_m1)_=_((H_`2)_._m2)_*_((H_`2)_._m1)
let m1, m2 be Morphism of C; ::_thesis: ( dom m2 = cod m1 implies (H `2) . (m2 (*) m1) = ((H `2) . m2) * ((H `2) . m1) )
assume  dom m2 = cod m1 ; ::_thesis: (H `2) . (m2 (*) m1) = ((H `2) . m2) * ((H `2) . m1)
A3: (H `2) . m1 = id D by A1, FUNCOP_1:7;
 ( (H `2) . (m2 (*) m1) = id D & (H `2) . m2 = id D ) by A1, FUNCOP_1:7;
hence  (H `2) . (m2 (*) m1) = ((H `2) . m2) * ((H `2) . m1) by A3, FUNCT_2:17; ::_thesis: verum
end;
hence  [( the carrier of C --> D),( the carrier' of C --> (id D))] is Indexing of C by A2, Th6; ::_thesis: [( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C
 for m being Morphism of C holds (H `2) . m is Functor of ((H `1) * the Target of C) . m,((H `1) * the Source of C) . m by Lm5;
then  H `2 is ManySortedFunctor of (H `1) * the Target of C,(H `1) * the Source of C by Def7;
then reconsider H = H as Indexing of the Target of C, the Source of C by Def8;
now__::_thesis:_for_m1,_m2_being_Morphism_of_C_st_dom_m2_=_cod_m1_holds_
(H_`2)_._(m2_(*)_m1)_=_((H_`2)_._m1)_*_((H_`2)_._m2)
let m1, m2 be Morphism of C; ::_thesis: ( dom m2 = cod m1 implies (H `2) . (m2 (*) m1) = ((H `2) . m1) * ((H `2) . m2) )
assume  dom m2 = cod m1 ; ::_thesis: (H `2) . (m2 (*) m1) = ((H `2) . m1) * ((H `2) . m2)
A4: (H `2) . m1 = id D by A1, FUNCOP_1:7;
 ( (H `2) . (m2 (*) m1) = id D & (H `2) . m2 = id D ) by A1, FUNCOP_1:7;
hence  (H `2) . (m2 (*) m1) = ((H `2) . m1) * ((H `2) . m2) by A4, FUNCT_2:17; ::_thesis: verum
end;
hence  [( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C by A2, Th7; ::_thesis: verum
end;

begin

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
let x be set ; :: according to INDEX_1:def_1 ::_thesis: ( x in dom (Obj F) implies (Obj F) . x is Category )
assume  x in dom (Obj F) ; ::_thesis: (Obj F) . x is Category
then  ( rng (Obj F) c= the carrier of D & (Obj F) . x in rng (Obj F) ) by FUNCT_1:def_3, RELAT_1:def_19;
hence  (Obj F) . x is Category by CAT_5:12; ::_thesis: verum
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
let C be Category; ::_thesis: for D being Categorial Category
for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C
let D be Categorial Category; ::_thesis: for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C
let F be Functor of C,D; ::_thesis: [(Obj F),(pr2 F)] is Indexing of C
set I = [(Obj F),(pr2 F)];
A1: [(Obj F),(pr2 F)] `1 = Obj F ;
A2: dom F = the carrier' of C by FUNCT_2:def_1;
 dom (Obj F) = the carrier of C by FUNCT_2:def_1;
then A3: Obj F is ManySortedSet of the carrier of C by PARTFUN1:def_2;
A4: [(Obj F),(pr2 F)] `2 = pr2 F ;
A5: dom (pr2 F) = dom F by MCART_1:def_13;
then  pr2 F is ManySortedSet of the carrier' of C by A2, PARTFUN1:def_2, RELAT_1:def_18;
then reconsider I = [(Obj F),(pr2 F)] as ManySortedSet of the carrier of C, the carrier' of C by A3, Def4;
 pr2 F is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 (pr2 F) or (pr2 F) . x is set )
assume  x in dom (pr2 F) ; ::_thesis: (pr2 F) . x is set
then reconsider x = x as Morphism of C by A2, MCART_1:def_13;
reconsider m = F . x as Morphism of D ;
 (pr2 F) . x = m `2 by A2, MCART_1:def_13;
hence  (pr2 F) . x is set ; ::_thesis: verum
end;
then reconsider FF = pr2 F as ManySortedFunction of the carrier' of C by A5, A2, PARTFUN1:def_2, RELAT_1:def_18;
 I `1 is Category-yielding by MCART_1:7;
then reconsider I = I as Category-yielding_on_first ManySortedSet of the carrier of C, the carrier' of C by Def5;
 FF is ManySortedFunctor of (I `1) * the Source of C,(I `1) * the Target of C
proof
let m be Morphism of C; :: according to INDEX_1:def_7 ::_thesis: FF . m is Functor of ((I `1) * the Source of C) . m,((I `1) * the Target of C) . m
reconsider x = F . m as Morphism of D ;
A6: x `11 = dom (F . m) by CAT_5:13;
 x `12 = cod (F . m) by CAT_5:13;
then consider f being Functor of x `11 ,x `12  such that
A7: F . m = [[(x `11),(x `12)],f] by A6, CAT_5:def_6;
A8: ((Obj F) * the Source of C) . m = (Obj F) . (dom m) by FUNCT_2:15
.= dom (F . m) by CAT_1:69 ;
A9: ((Obj F) * the Target of C) . m = (Obj F) . (cod m) by FUNCT_2:15
.= cod (F . m) by CAT_1:69 ;
FF . m = x `2 by A2, MCART_1:def_13
.= f by A7, MCART_1:7 ;
hence  FF . m is Functor of ((I `1) * the Source of C) . m,((I `1) * the Target of C) . m by A1, A6, A8, A9, CAT_5:13; ::_thesis: verum
end;
then reconsider I = I as Indexing of the Source of C, the Target of C by A4, Def8;
A10: dom F = the carrier' of C by FUNCT_2:def_1;
A11: now__::_thesis:_for_m1,_m2_being_Morphism_of_C_st_dom_m2_=_cod_m1_holds_
(I_`2)_._(m2_(*)_m1)_=_((I_`2)_._m2)_*_((I_`2)_._m1)
let m1, m2 be Morphism of C; ::_thesis: ( dom m2 = cod m1 implies (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) )
assume A12: dom m2 = cod m1 ; ::_thesis: (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)
set h1 = F . m1;
set h2 = F . m2;
A13: dom (F . m2) = F . (dom m2) by CAT_1:72
.= cod (F . m1) by A12, CAT_1:72 ;
A14: dom (F . m2) = (F . m2) `11 by CAT_5:13;
 cod (F . m2) = (F . m2) `12 by CAT_5:13;
then consider f2 being Functor of (F . m2) `11 ,(F . m2) `12  such that
A15: F . m2 = [[((F . m2) `11),((F . m2) `12)],f2] by A14, CAT_5:def_6;
A16: cod (F . m1) = (F . m1) `12 by CAT_5:13;
 dom (F . m1) = (F . m1) `11 by CAT_5:13;
then consider f1 being Functor of (F . m1) `11 ,(F . m1) `12  such that
A17: F . m1 = [[((F . m1) `11),((F . m1) `12)],f1] by A16, CAT_5:def_6;
thus (I `2) . (m2 (*) m1) = (F . (m2 (*) m1)) `2 by A4, A10, MCART_1:def_13
.= ((F . m2) (*) (F . m1)) `2 by A12, CAT_1:64
.= [[((F . m1) `11),((F . m2) `12)],(f2 * f1)] `2 by A14, A16, A15, A17, A13, CAT_5:def_6
.= f2 * f1
.= ((F . m2) `2) * f1 by A15, MCART_1:7
.= ((F . m2) `2) * ((F . m1) `2) by A17, MCART_1:7
.= ((I `2) . m2) * ((F . m1) `2) by A4, A10, MCART_1:def_13
.= ((I `2) . m2) * ((I `2) . m1) by A4, A10, MCART_1:def_13 ; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Object_of_C_holds_(I_`2)_._(id_a)_=_id_((I_`1)_._a)
let a be Object of C; ::_thesis: (I `2) . (id a) = id ((I `1) . a)
reconsider i = (Obj F) . a as Object of D ;
thus (I `2) . (id a) = (F . (id a)) `2 by A4, A10, MCART_1:def_13
.= (id i) `2 by CAT_1:68
.= [[((I `1) . a),((I `1) . a)],(id ((I `1) . a))] `2 by A1, CAT_5:def_6
.= id ((I `1) . a) ; ::_thesis: verum
end;
hence  [(Obj F),(pr2 F)] is Indexing of C by A11, Th6; ::_thesis: verum
end;

definition
let C be Category;
let D be Categorial Category;
let F be Functor of C,D;
funcF -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
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
let C be Category; ::_thesis: for D being Categorial Category
for F being Functor of C,D holds D is TargetCat of F -indexing_of C
let D be Categorial Category; ::_thesis: for F being Functor of C,D holds D is TargetCat of F -indexing_of C
let F be Functor of C,D; ::_thesis: D is TargetCat of F -indexing_of C
set I = F -indexing_of C;
A1: (F -indexing_of C) `1 = Obj F by MCART_1:7;
hence  for a being Object of C holds ((F -indexing_of C) `1) . a is Object of D by FUNCT_2:5; :: according to INDEX_1:def_9 ::_thesis: for b being Element of the carrier' of C holds [[(((F -indexing_of C) `1) . ( the Source of C . b)),(((F -indexing_of C) `1) . ( the Target of C . b))],(((F -indexing_of C) `2) . b)] is Morphism of D
let b be Morphism of C; ::_thesis: [[(((F -indexing_of C) `1) . ( the Source of C . b)),(((F -indexing_of C) `1) . ( the Target of C . b))],(((F -indexing_of C) `2) . b)] is Morphism of D
set h = F . b;
A2: dom (F . b) = (F . b) `11 by CAT_5:13;
 cod (F . b) = (F . b) `12 by CAT_5:13;
then consider f being Functor of (F . b) `11 ,(F . b) `12  such that
A3: F . b = [[((F . b) `11),((F . b) `12)],f] by A2, CAT_5:def_6;
A4: cod (F . b) = (Obj F) . (cod b) by CAT_1:69
.= (Obj F) . ( the Target of C . b) ;
A5: dom (F . b) = (Obj F) . (dom b) by CAT_1:69
.= (Obj F) . ( the Source of C . b) ;
 ( (F -indexing_of C) `2 = pr2 F & dom F = the carrier' of C ) by FUNCT_2:def_1, MCART_1:7;
then ((F -indexing_of C) `2) . b = (F . b) `2 by MCART_1:def_13
.= f by A3, MCART_1:7 ;
hence  [[(((F -indexing_of C) `1) . ( the Source of C . b)),(((F -indexing_of C) `1) . ( the Target of C . b))],(((F -indexing_of C) `2) . b)] is Morphism of D by A1, A2, A3, A5, A4, CAT_5:13; ::_thesis: verum
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
let C be Category; ::_thesis: 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)
let D be Categorial Category; ::_thesis: 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)
let F be Functor of C,D; ::_thesis: for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)
set I = F -indexing_of C;
let T be TargetCat of F -indexing_of C; ::_thesis: F = (F -indexing_of C) -functor (C,T)
A1: (F -indexing_of C) `2 = pr2 F by MCART_1:7;
A2: dom F = the carrier' of C by FUNCT_2:def_1;
A3: (F -indexing_of C) `1 = Obj F by MCART_1:7;
A4: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C_holds_
F_._x_=_((F_-indexing_of_C)_-functor_(C,T))_._x
let x be set ; ::_thesis: ( x in the carrier' of C implies F . x = ((F -indexing_of C) -functor (C,T)) . x )
assume  x in the carrier' of C ; ::_thesis: F . x = ((F -indexing_of C) -functor (C,T)) . x
then reconsider f = x as Morphism of C ;
set h = F . f;
A5: ( dom (F . f) = (Obj F) . (dom f) & cod (F . f) = (Obj F) . (cod f) ) by CAT_1:69;
A6: ( dom (F . f) = (F . f) `11 & cod (F . f) = (F . f) `12 ) by CAT_5:13;
then consider g being Functor of (F . f) `11 ,(F . f) `12  such that
A7: F . f = [[((F . f) `11),((F . f) `12)],g] by CAT_5:def_6;
((F -indexing_of C) `2) . f = (F . f) `2 by A1, A2, MCART_1:def_13
.= g by A7, MCART_1:7 ;
hence  F . x = ((F -indexing_of C) -functor (C,T)) . x by A3, A6, A7, A5, Def11; ::_thesis: verum
end;
 dom ((F -indexing_of C) -functor (C,T)) = the carrier' of C by FUNCT_2:def_1;
hence  F = (F -indexing_of C) -functor (C,T) by A2, A4, FUNCT_1:2; ::_thesis: verum
end;

theorem :: 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
let C be Category; ::_thesis: for I being Indexing of C
for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2
let I be Indexing of C; ::_thesis: for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2
let T be TargetCat of I; ::_thesis: pr2 (I -functor (C,T)) = I `2
A1: dom (I -functor (C,T)) = the carrier' of C by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C_holds_
(pr2_(I_-functor_(C,T)))_._x_=_(I_`2)_._x
let x be set ; ::_thesis: ( x in the carrier' of C implies (pr2 (I -functor (C,T))) . x = (I `2) . x )
assume  x in the carrier' of C ; ::_thesis: (pr2 (I -functor (C,T))) . x = (I `2) . x
then reconsider f = x as Morphism of C ;
 (I -functor (C,T)) . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] by Def11;
then  ((I -functor (C,T)) . x) `2 = (I `2) . f by MCART_1:7;
hence  (pr2 (I -functor (C,T))) . x = (I `2) . x by A1, MCART_1:def_13; ::_thesis: verum
end;
 ( dom (pr2 (I -functor (C,T))) = dom (I -functor (C,T)) & dom (I `2) = the carrier' of C ) by MCART_1:def_13, PARTFUN1:def_2;
hence  pr2 (I -functor (C,T)) = I `2 by A1, A2, FUNCT_1:2; ::_thesis: verum
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
let C be Category; ::_thesis: for I being Indexing of C
for T being TargetCat of I holds (I -functor (C,T)) -indexing_of C = I
let I be Indexing of C; ::_thesis: for T being TargetCat of I holds (I -functor (C,T)) -indexing_of C = I
let T be TargetCat of I; ::_thesis: (I -functor (C,T)) -indexing_of C = I
set F = I -functor (C,T);
A1: ex f being ManySortedSet of the carrier of C ex g being ManySortedSet of the carrier' of C st I = [f,g] by Def4;
thus (I -functor (C,T)) -indexing_of C = [(I `1),(pr2 (I -functor (C,T)))] by Lm3
.= [(I `1),(I `2)] by Th20
.= I by A1, MCART_1:8 ; ::_thesis: verum
end;

begin

Lm6: now__::_thesis:_for_c,_d_being_Category
for_e_being_Subcategory_of_d
for_f_being_Functor_of_c,e_holds_f_is_Functor_of_c,d
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
.= f by FUNCT_2:17 ;
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 ;
funcI * F ->  Indexing of C means :Def16: :: INDEX_1:def 16
 for F9 being Functor of C,E st F9 = F holds
it = ((I -functor (E,(rng I))) * F9) -indexing_of C;
existence
 ex b1 being Indexing of C st
for F9 being Functor of C,E st F9 = F holds
b1 = ((I -functor (E,(rng I))) * F9) -indexing_of C
proof
reconsider A = Image F as Subcategory of E by A1;
reconsider G = F as Functor of C,A by CAT_5:8;
reconsider G = G as Functor of C,E by Lm6;
take  ((I -functor (E,(rng I))) * G) -indexing_of C ; ::_thesis: for F9 being Functor of C,E st F9 = F holds
((I -functor (E,(rng I))) * G) -indexing_of C = ((I -functor (E,(rng I))) * F9) -indexing_of C
thus  for F9 being Functor of C,E st F9 = F holds
((I -functor (E,(rng I))) * G) -indexing_of C = ((I -functor (E,(rng I))) * F9) -indexing_of C ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Indexing of C st ( for F9 being Functor of C,E st F9 = F holds
b1 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds
b2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) holds
b1 = b2
proof
reconsider A = Image F as Subcategory of E by A1;
reconsider G = F as Functor of C,A by CAT_5:8;
let J1, J2 be Indexing of C; ::_thesis: ( ( for F9 being Functor of C,E st F9 = F holds
J1 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds
J2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) implies J1 = J2 )
assume that
A2: for F9 being Functor of C,E st F9 = F holds
J1 = ((I -functor (E,(rng I))) * F9) -indexing_of C and
A3: for F9 being Functor of C,E st F9 = F holds
J2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ; ::_thesis: J1 = J2
reconsider G = G as Functor of C,E by Lm6;
thus J1 = ((I -functor (E,(rng I))) * G) -indexing_of C by A2
.= J2 by A3 ; ::_thesis: verum
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 F9 being Functor of C,E st F9 = F holds
b6 = ((I -functor (E,(rng I))) * F9) -indexing_of C );

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
let C, D1, D2, E be Category; ::_thesis: 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
let I be Indexing of E; ::_thesis: 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
let F be Functor of C,D1; ::_thesis: 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
let G be Functor of C,D2; ::_thesis: ( Image F is Subcategory of E & Image G is Subcategory of E & F = G implies I * F = I * G )
assume that
A1: Image F is Subcategory of E and
A2: Image G is Subcategory of E and
A3: F = G ; ::_thesis: I * F = I * G
reconsider F9 = F as Functor of C, Image F by CAT_5:8;
reconsider F9 = F9 as Functor of C,E by A1, Lm6;
 I * F = ((I -functor (E,(rng I))) * F9) -indexing_of C by A1, Def16;
hence  I * F = I * G by A2, A3, Def16; ::_thesis: verum
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
let C, D be Category; ::_thesis: 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
let F be Functor of C,D; ::_thesis: for I being Indexing of D
for T being TargetCat of I holds I * F = ((I -functor (D,T)) * F) -indexing_of C
let I be Indexing of D; ::_thesis: for T being TargetCat of I holds I * F = ((I -functor (D,T)) * F) -indexing_of C
let T be TargetCat of I; ::_thesis: I * F = ((I -functor (D,T)) * F) -indexing_of C
 Image F is Subcategory of D ;
then A1: I * F = ((I -functor (D,(rng I))) * F) -indexing_of C by Def16;
 (I -functor (D,(rng I))) * F = (I -functor (D,T)) * F by Th11;
hence  I * F = ((I -functor (D,T)) * F) -indexing_of C by A1, Th2; ::_thesis: verum
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
let C, D be Category; ::_thesis: 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
let F be Functor of C,D; ::_thesis: for I being Indexing of D
for T being TargetCat of I holds T is TargetCat of I * F
let I be Indexing of D; ::_thesis: for T being TargetCat of I holds T is TargetCat of I * F
let T be TargetCat of I; ::_thesis: T is TargetCat of I * F
set T9 = the TargetCat of I * F;
 ( rng (I * F) = Image ((I * F) -functor (C, the TargetCat of I * F)) & I * F = ((I -functor (D,T)) * F) -indexing_of C ) by Def12, Th23;
then  rng (I * F) = Image ((I -functor (D,T)) * F) by Th18, CAT_5:22;
hence  T is TargetCat of I * F by Th14; ::_thesis: verum
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
let C, D be Category; ::_thesis: 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
let F be Functor of C,D; ::_thesis: for I being Indexing of D
for T being TargetCat of I holds rng (I * F) is Subcategory of T
let I be Indexing of D; ::_thesis: for T being TargetCat of I holds rng (I * F) is Subcategory of T
let T be TargetCat of I; ::_thesis: rng (I * F) is Subcategory of T
 T is TargetCat of I * F by Th24;
hence  rng (I * F) is Subcategory of T by Th14; ::_thesis: verum
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
let C, D, E be Category; ::_thesis: 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)
let F be Functor of C,D; ::_thesis: for G being Functor of D,E
for I being Indexing of E holds (I * G) * F = I * (G * F)
let G be Functor of D,E; ::_thesis: for I being Indexing of E holds (I * G) * F = I * (G * F)
let I be Indexing of E; ::_thesis: (I * G) * F = I * (G * F)
set T = rng I;
reconsider T9 = rng I as TargetCat of I * G by Th24;
 I * G = ((I -functor (E,(rng I))) * G) -indexing_of D by Th23;
then  (I * G) -functor (D,T9) = (I -functor (E,(rng I))) * G by Th18;
hence (I * G) * F = (((I -functor (E,(rng I))) * G) * F) -indexing_of C by Th23
.= ((I -functor (E,(rng I))) * (G * F)) -indexing_of C by RELAT_1:36
.= I * (G * F) by Th23 ;
::_thesis: verum
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;
funcF * 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
reconsider T = D as TargetCat of I by A1;
reconsider G = F as Functor of T,E ;
take  (G * (I -functor (C,T))) -indexing_of C ; ::_thesis: for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
(G * (I -functor (C,T))) -indexing_of C = (G * (I -functor (C,T))) -indexing_of C
thus  for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
(G * (I -functor (C,T))) -indexing_of C = (G * (I -functor (C,T))) -indexing_of C ; ::_thesis: verum
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
reconsider T = D as TargetCat of I by A1;
reconsider G = F as Functor of T,E ;
let J1, J2 be Indexing of C; ::_thesis: ( ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
J1 = (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
J2 = (G * (I -functor (C,T))) -indexing_of C ) implies J1 = J2 )
assume A1: ( ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
J1 = (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
J2 = (G * (I -functor (C,T))) -indexing_of C ) & not J1 = J2 ) ; ::_thesis: contradiction
then  J1 = (G * (I -functor (C,T))) -indexing_of C ;
hence  contradiction by A1; ::_thesis: verum
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
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
let C be Category; ::_thesis: 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
let I be Indexing of C; ::_thesis: 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
let T be TargetCat of I; ::_thesis: 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
let D, E be Categorial Category; ::_thesis: for F being Functor of T,D
for G being Functor of T,E st F = G holds
F * I = G * I
let F be Functor of T,D; ::_thesis: for G being Functor of T,E st F = G holds
F * I = G * I
let G be Functor of T,E; ::_thesis: ( F = G implies F * I = G * I )
assume A1: F = G ; ::_thesis: F * I = G * I
thus F * I = (F * (I -functor (C,T))) -indexing_of C by Def17
.= (G * (I -functor (C,T))) -indexing_of C by A1, Th2
.= G * I by Def17 ; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let I be Indexing of C; ::_thesis: 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
let T be TargetCat of I; ::_thesis: for D being Categorial Category
for F being Functor of T,D holds Image F is TargetCat of F * I
let D be Categorial Category; ::_thesis: for F being Functor of T,D holds Image F is TargetCat of F * I
let F be Functor of T,D; ::_thesis: Image F is TargetCat of F * I
reconsider F9 = F as Functor of T, Image F by CAT_5:8;
set T9 = the TargetCat of F * I;
A1: rng (F * I) = Image ((F * I) -functor (C, the TargetCat of F * I)) by Def12;
F * I = F9 * I by Th27
.= (F9 * (I -functor (C,T))) -indexing_of C by Def17 ;
then  rng (F * I) = Image (F9 * (I -functor (C,T))) by A1, Th18, CAT_5:22;
hence  Image F is TargetCat of F * I by Th14; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let I be Indexing of C; ::_thesis: 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
let T be TargetCat of I; ::_thesis: for D being Categorial Category
for F being Functor of T,D holds D is TargetCat of F * I
let D be Categorial Category; ::_thesis: for F being Functor of T,D holds D is TargetCat of F * I
let F be Functor of T,D; ::_thesis: D is TargetCat of F * I
 Image F is TargetCat of F * I by Th28;
then  rng (F * I) is Subcategory of Image F by Th14;
then  rng (F * I) is Subcategory of D by CAT_5:4;
hence  D is TargetCat of F * I by Th14; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let I be Indexing of C; ::_thesis: 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
let T be TargetCat of I; ::_thesis: for D being Categorial Category
for F being Functor of T,D holds rng (F * I) is Subcategory of Image F
let D be Categorial Category; ::_thesis: for F being Functor of T,D holds rng (F * I) is Subcategory of Image F
let F be Functor of T,D; ::_thesis: rng (F * I) is Subcategory of Image F
 Image F is TargetCat of F * I by Th28;
hence  rng (F * I) is Subcategory of Image F by Th14; ::_thesis: verum
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
let C be Category; ::_thesis: 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)
let I be Indexing of C; ::_thesis: 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)
let T be TargetCat of I; ::_thesis: 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)
let D, E be Categorial Category; ::_thesis: for F being Functor of T,D
for G being Functor of D,E holds (G * F) * I = G * (F * I)
let F be Functor of T,D; ::_thesis: for G being Functor of D,E holds (G * F) * I = G * (F * I)
reconsider D9 = D as TargetCat of F * I by Th29;
let G be Functor of D,E; ::_thesis: (G * F) * I = G * (F * I)
reconsider G9 = G as Functor of D9,E ;
 F * I = (F * (I -functor (C,T))) -indexing_of C by Def17;
then A1: (F * I) -functor (C,D9) = F * (I -functor (C,T)) by Th18;
thus (G * F) * I = ((G * F) * (I -functor (C,T))) -indexing_of C by Def17
.= (G9 * ((F * I) -functor (C,D9))) -indexing_of C by A1, RELAT_1:36
.= G * (F * I) by Def17 ; ::_thesis: verum
end;

definition
let C, D be Category;
let I1 be Indexing of C;
let I2 be Indexing of D;
funcI2 * 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
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
let C be Category; ::_thesis: 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))
let D be Categorial Category; ::_thesis: 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))
let I1 be Indexing of C; ::_thesis: 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))
let I2 be Indexing of D; ::_thesis: for T being TargetCat of I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor (C,T))
let T be TargetCat of I1; ::_thesis: ( D is TargetCat of I1 implies I2 * I1 = I2 * (I1 -functor (C,T)) )
assume  D is TargetCat of I1 ; ::_thesis: I2 * I1 = I2 * (I1 -functor (C,T))
then reconsider D9 = D as TargetCat of I1 ;
A1: Image (I1 -functor (C,(rng I1))) = rng I1 by Def12;
 ( Image (I1 -functor (C,D9)) = rng I1 & Image (I1 -functor (C,T)) = rng I1 ) by Def12;
hence  I2 * I1 = I2 * (I1 -functor (C,T)) by A1, Th11, Th22; ::_thesis: verum
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
let C be Category; ::_thesis: 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
let D be Categorial Category; ::_thesis: 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
let I1 be Indexing of C; ::_thesis: 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
let I2 be Indexing of D; ::_thesis: for T being TargetCat of I2 st D is TargetCat of I1 holds
I2 * I1 = (I2 -functor (D,T)) * I1
let T be TargetCat of I2; ::_thesis: ( D is TargetCat of I1 implies I2 * I1 = (I2 -functor (D,T)) * I1 )
assume  D is TargetCat of I1 ; ::_thesis: I2 * I1 = (I2 -functor (D,T)) * I1
then reconsider D9 = D as TargetCat of I1 ;
reconsider I29 = I2 as Indexing of D9 ;
reconsider T9 = T as TargetCat of I29 ;
 ( Image (I1 -functor (C,D9)) = rng I1 & Image (I1 -functor (C,(rng I1))) = rng I1 ) by Def12;
hence I2 * I1 = I2 * (I1 -functor (C,D9)) by Th11, Th22
.= ((I29 -functor (D9,T9)) * (I1 -functor (C,D9))) -indexing_of C by Th23
.= (I2 -functor (D,T)) * I1 by Def17 ;
::_thesis: verum
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
let C, D be Category; ::_thesis: 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)
let F be Functor of C,D; ::_thesis: 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)
let I be Indexing of D; ::_thesis: 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)
let T be TargetCat of I; ::_thesis: for E being Categorial Category
for G being Functor of T,E holds (G * I) * F = G * (I * F)
reconsider T9 = T as TargetCat of I * F by Th24;
let E be Categorial Category; ::_thesis: for G being Functor of T,E holds (G * I) * F = G * (I * F)
let G be Functor of T,E; ::_thesis: (G * I) * F = G * (I * F)
reconsider G9 = G as Functor of T9,E ;
reconsider GI = rng (G * I) as TargetCat of (G * (I -functor (D,T))) -indexing_of D by Def17;
A1: I * F = ((I -functor (D,T)) * F) -indexing_of C by Th23;
A2: ((G * (I -functor (D,T))) -indexing_of D) -functor (D,GI) = G * (I -functor (D,T)) by Th18;
 ( G * I = (G * (I -functor (D,T))) -indexing_of D & Image F is Subcategory of D ) by Def17;
hence (G * I) * F = ((((G * (I -functor (D,T))) -indexing_of D) -functor (D,GI)) * F) -indexing_of C by Def16
.= ((G * (I -functor (D,T))) * F) -indexing_of C by A2, Th2
.= (G * ((I -functor (D,T)) * F)) -indexing_of C by RELAT_1:36
.= (G9 * ((I * F) -functor (C,T9))) -indexing_of C by A1, Th18
.= G * (I * F) by Def17 ;
::_thesis: verum
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
let C be Category; ::_thesis: 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)
let I be Indexing of C; ::_thesis: 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)
let T be TargetCat of I; ::_thesis: 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)
let D be Categorial Category; ::_thesis: for F being Functor of T,D
for J being Indexing of D holds (J * F) * I = J * (F * I)
let F be Functor of T,D; ::_thesis: for J being Indexing of D holds (J * F) * I = J * (F * I)
let J be Indexing of D; ::_thesis: (J * F) * I = J * (F * I)
A1: ( F * I = (F * (I -functor (C,T))) -indexing_of C & Image (F * (I -functor (C,T))) is Subcategory of D ) by Def17;
 D is TargetCat of F * I by Th29;
then  rng (F * I) is Subcategory of D by Th14;
then A2: Image ((F * I) -functor (C,(rng (F * I)))) is Subcategory of D by CAT_5:4;
thus (J * F) * I = (J * F) * (I -functor (C,T)) by Th32
.= J * (F * (I -functor (C,T))) by Th26
.= J * (F * I) by A1, A2, Th18, Th22 ; ::_thesis: verum
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
let C be Category; ::_thesis: 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)
let I be Indexing of C; ::_thesis: 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)
let T1 be TargetCat of I; ::_thesis: 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)
let J be Indexing of T1; ::_thesis: 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)
let T2 be TargetCat of J; ::_thesis: for D being Categorial Category
for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let D be Categorial Category; ::_thesis: for F being Functor of T2,D holds (F * J) * I = F * (J * I)
let F be Functor of T2,D; ::_thesis: (F * J) * I = F * (J * I)
thus (F * J) * I = (F * J) * (I -functor (C,T1)) by Th32
.= F * (J * (I -functor (C,T1))) by Th34
.= F * (J * I) by Th32 ; ::_thesis: verum
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
let C, D be Category; ::_thesis: 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)
let F be Functor of C,D; ::_thesis: 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)
let I be Indexing of D; ::_thesis: for T being TargetCat of I
for J being Indexing of T holds (J * I) * F = J * (I * F)
let T be TargetCat of I; ::_thesis: for J being Indexing of T holds (J * I) * F = J * (I * F)
let J be Indexing of T; ::_thesis: (J * I) * F = J * (I * F)
A1: ( I * F = ((I -functor (D,T)) * F) -indexing_of C & Image ((I -functor (D,T)) * F) is Subcategory of T ) by Th23;
 T is TargetCat of I * F by Th24;
then  rng (I * F) is Subcategory of T by Th14;
then A2: Image ((I * F) -functor (C,(rng (I * F)))) is Subcategory of T by CAT_5:4;
thus (J * I) * F = (J * (I -functor (D,T))) * F by Th32
.= J * ((I -functor (D,T)) * F) by Th26
.= J * (I * F) by A1, A2, Th18, Th22 ; ::_thesis: verum
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
let C be Category; ::_thesis: 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)
let I be Indexing of C; ::_thesis: 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)
let D be TargetCat of I; ::_thesis: 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)
let J be Indexing of D; ::_thesis: for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)
let E be TargetCat of J; ::_thesis: for K being Indexing of E holds (K * J) * I = K * (J * I)
let K be Indexing of E; ::_thesis: (K * J) * I = K * (J * I)
thus (K * J) * I = (K * J) * (I -functor (C,D)) by Th32
.= K * (J * (I -functor (C,D))) by Th37
.= K * (J * I) by Th32 ; ::_thesis: verum
end;

theorem :: INDEX_1:39
for C being Category holds IdMap C = IdMap (C opp) by Lm2;