index_1.miz



    begin

    registration

      let A be non empty set;

      cluster non empty-yielding for ManySortedSet of A;

      existence

      proof

        take the non-empty ManySortedSet of A;

        take the Element of A;

        thus thesis;

      end;

    end

    definition

      let C be Categorial Category;

      let f be Morphism of C;

      :: original: `2

      redefine

      func f `2 -> Functor of (f `11 ), (f `12 ) ;

      coherence

      proof

        

         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;

      end;

    end

    theorem :: INDEX_1:1

    for C be Categorial Category, f,g be 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;

      let f,g be Morphism of C;

      

       A1: (g `11 ) = ( dom g) by CAT_5: 13;

      

       A2: (f `11 ) = ( dom f) by CAT_5: 13;

      assume

       A3: ( dom g) = ( cod f);

      then

      consider ff be 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 be 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

      .= [ [( dom f), ( cod g)], ((g `2 ) * (f `2 ))] by A6;

    end;

    theorem :: INDEX_1:2

    

     Th2: for C be Category, D,E be Categorial Category holds for F be Functor of C, D holds for G be Functor of C, E st F = G holds ( Obj F) = ( Obj G)

    proof

      let C be Category, D,E be Categorial Category;

      let F be Functor of C, D;

      let G be Functor of C, E such that

       A1: F = G;

       A2:

      now

        let x be object;

        assume x in the carrier of C;

        then

        reconsider a = x as Object of C;

        

         A3: a = ( dom ( id a));

        

        hence (( Obj F) . x) = ( dom (F . ( id a) qua Morphism of C)) by CAT_1: 69

        .= ((F . ( id a) qua Morphism of C) `11 ) by CAT_5: 13

        .= ( dom (G . ( id a) qua Morphism of C)) by A1, CAT_5: 13

        .= (( Obj G) . x) by A3, CAT_1: 69;

      end;

      thus thesis by A2;

    end;

    definition

      let IT be Function;

      :: INDEX_1:def1

      attr IT is Category-yielding means

      : Def1: for x be set st x in ( dom IT) holds (IT . x) is Category;

    end

    registration

      cluster Category-yielding for Function;

      existence

      proof

        take f = ( {} --> ( 1Cat ( {} , { {} })));

        let x be set;

        assume x in ( dom f);

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster Category-yielding for ManySortedSet of X;

      existence

      proof

        take f = (X --> ( 1Cat ( {} , { {} })));

        let x be set;

        assume x in ( dom f);

        then x in X;

        hence thesis by FUNCOP_1: 7;

      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, x be Category;

      cluster (X --> x) -> Category-yielding;

      coherence by FUNCOP_1: 7;

    end

    registration

      let X be non empty set;

      cluster -> non empty for ManySortedSet of X;

      coherence ;

    end

    registration

      let f be Category-yielding Function;

      cluster ( rng f) -> categorial;

      coherence

      proof

        let x be set;

        assume x in ( rng f);

        then ex y be object st y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

        hence thesis by Def1;

      end;

    end

    definition

      let X be non empty set;

      let f be ManySortedCategory of X;

      let x be Element of X;

      :: original: .

      redefine

      func f . x -> Category ;

      coherence

      proof

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by Def1;

      end;

    end

    registration

      let f be Function;

      let g be Category-yielding Function;

      cluster (g * f) -> Category-yielding;

      coherence

      proof

        let x be set;

        assume x in ( dom (g * f));

        then ((g * f) . x) = (g . (f . x)) & (f . x) in ( dom g) by FUNCT_1: 11, FUNCT_1: 12;

        hence thesis by Def1;

      end;

    end

    definition

      let F be Category-yielding Function;

      :: INDEX_1:def2

      func Objs F -> non-empty Function means

      : Def2: ( dom it ) = ( dom F) & for x be object st x in ( dom F) holds for C be Category st C = (F . x) holds (it . x) = the carrier of C;

      existence

      proof

        defpred P[ object, object] means for C be Category st C = (F . $1) holds $2 = the carrier of C;

         A1:

        now

          let x be object;

          assume x in ( dom F);

          then

          reconsider C = (F . x) as Category by Def1;

          reconsider y = the carrier of C as object;

          take y;

          thus P[x, y];

        end;

        consider f be Function such that

         A2: ( dom f) = ( dom F) & for x be object st x in ( dom F) holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        f is non-empty

        proof

          let x be object;

          assume

           A3: x in ( dom f);

          then

          reconsider C = (F . x) as Category by A2, Def1;

          (f . x) = the carrier of C by A2, A3;

          hence thesis;

        end;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be non-empty Function such that

         A4: ( dom f1) = ( dom F) and

         A5: for x be object st x in ( dom F) holds for C be Category st C = (F . x) holds (f1 . x) = the carrier of C and

         A6: ( dom f2) = ( dom F) and

         A7: for x be object st x in ( dom F) holds for C be Category st C = (F . x) holds (f2 . x) = the carrier of C;

        now

          let x be object;

          assume

           A8: x in ( dom F);

          then

          reconsider C = (F . x) as Category by Def1;

          

          thus (f1 . x) = the carrier of C by A5, A8

          .= (f2 . x) by A7, A8;

        end;

        hence thesis by A4, A6;

      end;

      :: INDEX_1:def3

      func Mphs F -> non-empty Function means

      : Def3: ( dom it ) = ( dom F) & for x be object st x in ( dom F) holds for C be Category st C = (F . x) holds (it . x) = the carrier' of C;

      existence

      proof

        defpred P[ object, object] means for C be Category st C = (F . $1) holds $2 = the carrier' of C;

         A9:

        now

          let x be object;

          assume x in ( dom F);

          then

          reconsider C = (F . x) as Category by Def1;

          reconsider y = the carrier' of C as object;

          take y;

          thus P[x, y];

        end;

        consider f be Function such that

         A10: ( dom f) = ( dom F) & for x be object st x in ( dom F) holds P[x, (f . x)] from CLASSES1:sch 1( A9);

        f is non-empty

        proof

          let x be object;

          assume

           A11: x in ( dom f);

          then

          reconsider C = (F . x) as Category by A10, Def1;

          (f . x) = the carrier' of C by A10, A11;

          hence thesis;

        end;

        hence thesis by A10;

      end;

      uniqueness

      proof

        let f1,f2 be non-empty Function such that

         A12: ( dom f1) = ( dom F) and

         A13: for x be object st x in ( dom F) holds for C be Category st C = (F . x) holds (f1 . x) = the carrier' of C and

         A14: ( dom f2) = ( dom F) and

         A15: for x be object st x in ( dom F) holds for C be Category st C = (F . x) holds (f2 . x) = the carrier' of C;

        now

          let x be object;

          assume

           A16: x in ( dom F);

          then

          reconsider C = (F . x) as Category by Def1;

          

          thus (f1 . x) = the carrier' of C by A13, A16

          .= (f2 . x) by A15, A16;

        end;

        hence thesis by A12, A14;

      end;

    end

    registration

      let A be non empty set;

      let F be ManySortedCategory of A;

      cluster ( Objs F) -> A -defined;

      coherence

      proof

        ( dom ( Objs F)) = ( dom F) by Def2

        .= A by PARTFUN1:def 2;

        hence thesis by RELAT_1:def 18;

      end;

      cluster ( Mphs F) -> A -defined;

      coherence

      proof

        ( dom ( Mphs F)) = ( dom F) by Def3

        .= A by PARTFUN1:def 2;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let A be non empty set;

      let F be ManySortedCategory of A;

      cluster ( Objs F) -> total;

      coherence

      proof

        ( dom ( Objs F)) = ( dom F) by Def2

        .= A by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

      cluster ( Mphs F) -> total;

      coherence

      proof

        ( dom ( Mphs F)) = ( dom F) by Def3

        .= A by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: INDEX_1:3

    for X be set, C be Category holds ( Objs (X --> C)) = (X --> the carrier of C) & ( Mphs (X --> C)) = (X --> the carrier' of C)

    proof

      let X be set, C be Category;

      

       A2: ( dom ( Objs (X --> C))) = ( dom (X --> C)) by Def2;

      now

        let a be object;

        assume

         A3: a in ( dom ( Objs (X --> C)));

        then ((X --> C) . a) = C by A2, FUNCOP_1: 7;

        hence (( Objs (X --> C)) . a) = the carrier of C by A2, A3, Def2;

      end;

      hence ( Objs (X --> C)) = (X --> the carrier of C) by A2, FUNCOP_1: 11;

      

       A4: ( dom ( Mphs (X --> C))) = ( dom (X --> C)) by Def3;

      now

        let a be object;

        assume

         A5: a in ( dom ( Mphs (X --> C)));

        then ((X --> C) . a) = C by A4, FUNCOP_1: 7;

        hence (( Mphs (X --> C)) . a) = the carrier' of C by A4, A5, Def3;

      end;

      hence thesis by A4, FUNCOP_1: 11;

    end;

    begin

    definition

      let A,B be set;

      :: INDEX_1:def4

      mode ManySortedSet of A,B -> object means

      : Def4: ex f be ManySortedSet of A, g be ManySortedSet of B st it = [f, g];

      existence

      proof

        set f = the ManySortedSet of A, g = the ManySortedSet of B;

        take [f, g], f, g;

        thus thesis;

      end;

    end

    definition

      let A,B be set;

      let f be ManySortedSet of A;

      let g be ManySortedSet of B;

      :: original: [

      redefine

      func [f,g] -> ManySortedSet of A, B ;

      coherence

      proof

        take f, g;

        thus thesis;

      end;

    end

    registration

      let A,B be set;

      let X be ManySortedSet of A, B;

      cluster (X `1 ) -> Function-like Relation-like;

      coherence

      proof

        ex f be ManySortedSet of A, g be ManySortedSet of B st (X = [f, g]) by Def4;

        hence thesis;

      end;

      cluster (X `2 ) -> Function-like Relation-like;

      coherence

      proof

        ex f be ManySortedSet of A, g be ManySortedSet of B st (X = [f, g]) by Def4;

        hence thesis;

      end;

    end

    registration

      let A,B be set;

      let X be ManySortedSet of A, B;

      cluster (X `1 ) -> A -defined;

      coherence

      proof

        ex f be ManySortedSet of A, g be ManySortedSet of B st (X = [f, g]) by Def4;

        hence thesis;

      end;

      cluster (X `2 ) -> B -defined;

      coherence

      proof

        ex f be ManySortedSet of A, g be ManySortedSet of B st (X = [f, g]) by Def4;

        hence thesis;

      end;

    end

    registration

      let A,B be set;

      let X be ManySortedSet of A, B;

      cluster (X `1 ) -> total;

      coherence

      proof

        ex f be ManySortedSet of A, g be ManySortedSet of B st (X = [f, g]) by Def4;

        hence thesis;

      end;

      cluster (X `2 ) -> total;

      coherence

      proof

        ex f be ManySortedSet of A, g be ManySortedSet of B st (X = [f, g]) by Def4;

        hence thesis;

      end;

    end

    definition

      let A,B be set;

      let IT be ManySortedSet of A, B;

      :: INDEX_1:def5

      attr IT is Category-yielding_on_first means

      : Def5: (IT `1 ) is Category-yielding;

      :: INDEX_1:def6

      attr IT is Function-yielding_on_second means

      : Def6: (IT `2 ) is Function-yielding;

    end

    registration

      let A,B be set;

      cluster Category-yielding_on_first Function-yielding_on_second for ManySortedSet of A, B;

      existence

      proof

        set g = the ManySortedFunction of B;

        set f = the ManySortedCategory of A;

        reconsider X = [f, g] as ManySortedSet of A, B;

        take X;

        thus (X `1 ) is Category-yielding & (X `2 ) is Function-yielding;

      end;

    end

    registration

      let A,B be set;

      let X be Category-yielding_on_first ManySortedSet of A, B;

      cluster (X `1 ) -> Category-yielding;

      coherence by Def5;

    end

    registration

      let A,B be set;

      let X be Function-yielding_on_second ManySortedSet of A, B;

      cluster (X `2 ) -> Function-yielding;

      coherence by Def6;

    end

    registration

      let f be Function-yielding Function;

      cluster ( rng f) -> functional;

      coherence

      proof

        let x be object;

        assume x in ( rng f);

        then ex y be object st y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    definition

      let A,B be set;

      let f be ManySortedCategory of A;

      let g be ManySortedFunction of B;

      :: original: [

      redefine

      func [f,g] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of A, B ;

      coherence

      proof

        ( [f, g] `1 ) = f & ( [f, g] `2 ) = g;

        hence thesis by Def5, Def6;

      end;

    end

    definition

      let A be non empty set;

      let F,G be ManySortedCategory of A;

      :: INDEX_1:def7

      mode ManySortedFunctor of F,G -> ManySortedFunction of A means

      : Def7: for a be Element of A holds (it . a) is Functor of (F . a), (G . a);

      existence

      proof

        defpred P[ object, object] means ex a9 be Element of A, t be Functor of (F . a9), (G . a9) st $1 = a9 & $2 = t;

         A1:

        now

          let a be object;

          assume a in A;

          then

          reconsider a9 = a as Element of A;

          set f = the Functor of (F . a9), (G . a9);

          reconsider f as object;

          take f;

          thus P[a, f];

        end;

        consider f be Function such that

         A2: ( dom f) = A & for a be object st a in A holds P[a, (f . a)] from CLASSES1:sch 1( A1);

        f is Function-yielding

        proof

          let a be object;

          assume a in ( dom f);

          then ex a9 be Element of A, t be Functor of (F . a9), (G . a9) st a = a9 & (f . a) = t by A2;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of A by A2, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        let a be Element of A;

        ex a9 be Element of A, t be Functor of (F . a9), (G . a9) st a = a9 & (f . a) = t by A2;

        hence thesis;

      end;

    end

    scheme :: INDEX_1:sch1

    LambdaMSFr { A() -> non empty set , C1,C2() -> ManySortedCategory of A() , F( object) -> set } :

ex F be ManySortedFunctor of C1(), C2() st for a be Element of A() holds (F . a) = F(a)

      provided

       A1: for a be Element of A() holds F(a) is Functor of (C1() . a), (C2() . a);

      consider f be ManySortedSet of A() such that

       A2: for a be object st a in A() holds (f . a) = F(a) from PBOOLE:sch 4;

      f is Function-yielding

      proof

        let a be object;

        assume a in ( dom f);

        then

        reconsider a as Element of A() by PARTFUN1:def 2;

        (f . a) = F(a) by A2;

        hence thesis by A1;

      end;

      then

      reconsider f as ManySortedFunction of A();

      f is ManySortedFunctor of C1(), C2()

      proof

        let a be Element of A();

        (f . a) = F(a) by A2;

        hence thesis by A1;

      end;

      then

      reconsider f as ManySortedFunctor of C1(), C2();

      take f;

      thus thesis by A2;

    end;

    definition

      let A be non empty set;

      let F,G be ManySortedCategory of A;

      let f be ManySortedFunctor of F, G;

      let a be Element of A;

      :: original: .

      redefine

      func f . a -> Functor of (F . a), (G . a) ;

      coherence by Def7;

    end

    begin

    definition

      let A,B be non empty set;

      let F,G be Function of B, A;

      :: INDEX_1:def8

      mode Indexing of F,G -> Category-yielding_on_first ManySortedSet of A, B means

      : Def8: (it `2 ) is ManySortedFunctor of ((it `1 ) * F), ((it `1 ) * G);

      existence

      proof

        set g = the ManySortedCategory of A;

        set f = the ManySortedFunctor of (g * F), (g * G);

        take I = [g, f];

        thus thesis;

      end;

    end

    theorem :: INDEX_1:4

    

     Th4: for A,B be non empty set, F,G be Function of B, A holds for I be Indexing of F, G holds for m be 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, F,G be Function of B, A;

      let I be Indexing of F, G;

      reconsider H = (I `2 ) as ManySortedFunctor of ((I `1 ) * F), ((I `1 ) * G) by Def8;

      let m be Element of B;

      ( 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 thesis by A1, FUNCT_1: 12;

    end;

    theorem :: INDEX_1:5

    for C be Category, I be Indexing of the Source of C, the Target of C holds for m be 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

      func I `2 -> ManySortedFunctor of ((I `1 ) * F), ((I `1 ) * G) ;

      coherence by Def8;

    end

     Lm1:

    now

      let A,B be non empty set;

      let F,G be Function of B, A;

      let I be Indexing of F, G;

      consider C be full strict Categorial Category such that

       A1: the carrier of C = ( rng (I `1 )) by CAT_5: 20;

      take C;

      

       A2: ( dom (I `1 )) = A by PARTFUN1:def 2;

      hence for a be Element of A holds ((I `1 ) . a) is Object of C by A1, FUNCT_1:def 3;

      let b be Element of B;

      

       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;

    end;

    definition

      let A,B be non empty set;

      let F,G be Function of B, A;

      let I be Indexing of F, G;

      :: INDEX_1:def9

      mode TargetCat of I -> Categorial Category means

      : Def9: (for a be Element of A holds ((I `1 ) . a) is Object of it ) & for b be Element of B holds [ [((I `1 ) . (F . b)), ((I `1 ) . (G . b))], ((I `2 ) . b)] is Morphism of it ;

      existence

      proof

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

        hence thesis;

      end;

    end

    registration

      let A,B be non empty set;

      let F,G be Function of B, A;

      let I be Indexing of F, G;

      cluster full strict for TargetCat of I;

      existence

      proof

        consider C be full strict Categorial Category such that

         A1: (for a be Element of A holds ((I `1 ) . a) is Object of C) & for b be 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 thesis;

      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 be Category such that

       A1: C = CatStr (# A, B, F, G, c #);

      :: INDEX_1:def10

      mode Indexing of F,G,c,i -> Indexing of F, G means

      : Def10: (for a be Element of A holds ((it `2 ) . (i . a)) = ( id ((it `1 ) . a))) & for m1,m2 be Element of B st (F . m2) = (G . m1) holds ((it `2 ) . (c . [m2, m1])) = (((it `2 ) . m2) * ((it `2 ) . m1));

      existence

      proof

        set I2 = (B --> ( id C));

        set I1 = (A --> C);

        

         A2: ( [I1, I2] `1 ) = I1;

        

         A3: ( [I1, I2] `2 ) = I2;

        I2 is ManySortedFunctor of (I1 * F), (I1 * G)

        proof

          let a be Element of B;

          (I1 . (F . a)) = C & ( dom (I1 * F)) = B by PARTFUN1:def 2;

          then

           A4: (I2 . a) = ( id C) & ((I1 * F) . a) = C by FUNCT_1: 12;

          (I1 . (G . a)) = C & ( dom (I1 * G)) = B by PARTFUN1:def 2;

          hence thesis by A4, FUNCT_1: 12;

        end;

        then

        reconsider I = [I1, I2] as Indexing of F, G by A2, A3, Def8;

        take I;

        thus for a be Element of A holds ((I `2 ) . (i . a)) = ( id ((I `1 ) . a));

        let m1,m2 be Element of B;

        reconsider mm1 = m1, mm2 = m2 as Morphism of C by A1;

        assume (F . m2) = (G . 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 FUNCOP_1: 7, PARTFUN1: 4;

        thus thesis by A5, FUNCT_2: 17;

      end;

    end

    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 :: INDEX_1:6

    

     Th6: for C be Category, I be Indexing of the Source of C, the Target of C holds I is Indexing of C iff (for a be Object of C holds ((I `2 ) . ( id a)) = ( id ((I `1 ) . a))) & for m1,m2 be Morphism of C st ( dom m2) = ( cod m1) holds ((I `2 ) . (m2 (*) m1)) = (((I `2 ) . m2) * ((I `2 ) . m1))

    proof

      let C be Category;

      reconsider D = the CatStr of C as Category by CAT_5: 1;

      let I be Indexing of the Source of C, the Target of C;

      

       A1: D = CatStr (# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #);

      hereby

        assume

         A2: I is Indexing of C;

        thus for a be Object of C holds ((I `2 ) . ( id a)) = ( id ((I `1 ) . a))

        proof

          let a be Object of C;

          ( id a) = (( IdMap C) . a) by ISOCAT_1:def 12;

          hence thesis by A1, Def10, A2;

        end;

        let m1,m2 be Morphism of C;

        assume

         A3: ( dom m2) = ( cod 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;

      end;

      assume that

       A4: for a be Object of C holds ((I `2 ) . ( id a)) = ( id ((I `1 ) . a)) and

       A5: for m1,m2 be Morphism of C st ( dom m2) = ( cod m1) holds ((I `2 ) . (m2 (*) m1)) = (((I `2 ) . m2) * ((I `2 ) . m1));

      thus ex D be 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;

      hereby

        let a be Object of C;

        ( 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;

      end;

      let m1,m2 be Morphism of C;

      assume (the Source of C . m2) = (the Target of C . 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;

    end;

    theorem :: INDEX_1:7

    

     Th7: for C be Category, I be Indexing of the Target of C, the Source of C holds I is coIndexing of C iff (for a be Object of C holds ((I `2 ) . ( id a)) = ( id ((I `1 ) . a))) & for m1,m2 be Morphism of C st ( dom m2) = ( cod m1) holds ((I `2 ) . (m2 (*) m1)) = (((I `2 ) . m1) * ((I `2 ) . m2))

    proof

      let C be Category;

      let I be Indexing of the Target of C, the Source of C;

      

       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

        assume

         A2: I is coIndexing of C;

        thus for a be Object of C holds ((I `2 ) . ( id a)) = ( id ((I `1 ) . a))

        proof

          let a be Object of C;

          ( id a) = (( IdMap C) . a) by ISOCAT_1:def 12;

          hence thesis by A1, Def10, A2;

        end;

        let m1,m2 be Morphism of C;

        assume

         A3: ( dom m2) = ( cod m1);

        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;

      end;

      assume that

       A5: for a be Object of C holds ((I `2 ) . ( id a)) = ( id ((I `1 ) . a)) and

       A6: for m1,m2 be Morphism of C st ( dom m2) = ( cod m1) holds ((I `2 ) . (m2 (*) m1)) = (((I `2 ) . m1) * ((I `2 ) . m2));

      thus ex D be 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;

      hereby

        let a be Object of C;

        ( 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;

      end;

      let m1,m2 be Morphism of C;

      assume (the Target of C . m2) = (the Source of C . 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;

    end;

    

     Lm2: for C be Category holds ( IdMap C) = ( IdMap (C opp ))

    proof

      let C be Category;

      thus the carrier of C = the carrier of (C opp );

      let o be Element of the carrier of C;

      

      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);

    end;

    theorem :: INDEX_1:8

    for C be Category, x be set holds x is coIndexing of C iff x is Indexing of (C opp ) by Lm2;

    theorem :: INDEX_1:9

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

    proof

      let C be Category, I be Indexing of C;

      let c1,c2 be Object of C such that

       A1: ( Hom (c1,c2)) is non empty;

      let m be Morphism of c1, 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 thesis by A2, FUNCT_1: 12;

    end;

    theorem :: INDEX_1:10

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

    proof

      let C be Category, I be coIndexing of C;

      let c1,c2 be Object of C such that

       A1: ( Hom (c1,c2)) is non empty;

      let m be Morphism of c1, 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 thesis by A2, FUNCT_1: 12;

    end;

    definition

      let C be Category;

      let I be Indexing of C;

      let T be TargetCat of I;

      :: INDEX_1:def11

      func I -functor (C,T) -> Functor of C, T means

      : Def11: for f be Morphism of C holds (it . f) = [ [((I `1 ) . ( dom f)), ((I `1 ) . ( cod f))], ((I `2 ) . f)];

      existence

      proof

        

         A1: ( rng (I `1 )) c= the carrier of T

        proof

          let x be object;

          assume x in ( rng (I `1 ));

          then

          consider a be object such that

           A2: a in ( dom (I `1 )) and

           A3: x = ((I `1 ) . a) by FUNCT_1:def 3;

          reconsider a as Object of C by A2, PARTFUN1:def 2;

          ((I `1 ) . a) is Object of T by Def9;

          hence thesis by A3;

        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 O( Object of C) = (I1 . $1);

        deffunc F( Morphism of C) = [ [((I `1 ) . ( dom $1)), ((I `1 ) . ( cod $1))], ((I `2 ) . $1)];

         A4:

        now

          let f be Morphism of C;

          thus F(f) is Morphism of T by Def9;

          let g be Morphism of T;

          assume

           A5: g = F(f);

          

          hence ( dom g) = ( F(f) `11 ) by CAT_5: 13

          .= O(dom) by MCART_1: 85;

          

          thus ( cod g) = ( F(f) `12 ) by A5, CAT_5: 13

          .= O(cod) by MCART_1: 85;

        end;

         A6:

        now

          let f1,f2 be Morphism of C;

          let g1,g2 be Morphism of T;

          assume that

           A7: g1 = F(f1) & g2 = F(f2) and

           A8: ( dom f2) = ( cod f1);

          

           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 F((*)) = (g2 (*) g1) by A7, A8, A10, A9, CAT_5:def 6;

        end;

         A11:

        now

          let a be Object of C;

          

          thus F(id) = [ [(I1 . a), (I1 . a)], ( id ((I `1 ) . a))] by Th6

          .= ( id O(a)) by CAT_5:def 6;

        end;

        thus ex F be Functor of C, T st for f be Morphism of C holds (F . f) = F(f) from CAT_5:sch 3( A4, A11, A6);

      end;

      uniqueness

      proof

        let F1,F2 be Functor of C, T such that

         A12: for f be Morphism of C holds (F1 . f) = [ [((I `1 ) . ( dom f)), ((I `1 ) . ( cod f))], ((I `2 ) . f)] and

         A13: for f be Morphism of C holds (F2 . f) = [ [((I `1 ) . ( dom f)), ((I `1 ) . ( cod f))], ((I `2 ) . f)];

        now

          let f be Morphism of C;

          

          thus (F1 . f) = [ [((I `1 ) . ( dom f)), ((I `1 ) . ( cod f))], ((I `2 ) . f)] by A12

          .= (F2 . f) by A13;

        end;

        hence thesis;

      end;

    end

    

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

    proof

      let C be Category, I be Indexing of C;

      let T be TargetCat of I;

       A1:

      now

        let x be object;

        assume x in the carrier of C;

        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) qua Morphism of C)) by CAT_1: 68

        .= (((I -functor (C,T)) qua Function . ( 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;

      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 thesis by A1;

    end;

    theorem :: INDEX_1:11

    

     Th11: for C be Category, I be Indexing of C holds for T1,T2 be 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, I be Indexing of C;

      let T1,T2 be TargetCat of I;

       A1:

      now

        let x be object;

        assume x in the carrier' of C;

        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;

      end;

      thus (I -functor (C,T1)) = (I -functor (C,T2)) by A1;

       A2:

      now

        let x be object;

        assume x in the carrier of C;

        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;

      end;

      thus thesis by A2;

    end;

    theorem :: INDEX_1:12

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

    theorem :: INDEX_1:13

    for C be Category, I be Indexing of C holds for T be TargetCat of I, x be 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;

      :: INDEX_1:def12

      func rng I -> strict TargetCat of I means

      : Def12: for T be TargetCat of I holds it = ( Image (I -functor (C,T)));

      uniqueness

      proof

        set T = the TargetCat of I;

        let T1,T2 be strict TargetCat of I such that

         A1: for T be TargetCat of I holds T1 = ( Image (I -functor (C,T))) and

         A2: for T be TargetCat of I holds T2 = ( Image (I -functor (C,T)));

        

        thus T1 = ( Image (I -functor (C,T))) by A1

        .= T2 by A2;

      end;

      existence

      proof

        set S = the TargetCat of I;

        reconsider T = ( Image (I -functor (C,S))) as strict Subcategory of S;

        reconsider F = (I -functor (C,S)) as Functor of C, T by CAT_5: 8;

        T is TargetCat of I

        proof

          the carrier of T = ( rng ( Obj (I -functor (C,S)))) 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 be Object of C holds ((I `1 ) . a) is Object of T by A3, FUNCT_1:def 3;

          let b be Morphism of C;

          (F . b) = [ [((I `1 ) . ( dom b)), ((I `1 ) . ( cod b))], ((I `2 ) . b)] by Def11;

          hence thesis;

        end;

        then

        reconsider T as strict TargetCat of I;

        take T;

        let T9 be TargetCat of I;

        thus thesis by Th11, CAT_5: 22;

      end;

    end

    theorem :: INDEX_1:14

    

     Th14: for C be Category, I be Indexing of C holds for D be Categorial Category holds ( rng I) is Subcategory of D iff D is TargetCat of I

    proof

      let C be Category, I be Indexing of C;

      let D be Categorial Category;

      hereby

        assume

         A1: ( rng I) is Subcategory of D;

        thus D is TargetCat of I

        proof

          hereby

            let a be Object of C;

            ((I `1 ) . a) is Object of ( rng I) by Def9;

            hence ((I `1 ) . a) is Object of D by A1, CAT_2: 6;

          end;

          let b be Morphism of C;

           [ [((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 thesis by A1, CAT_2: 8;

        end;

      end;

      assume D is TargetCat of I;

      then

      reconsider T = D as TargetCat of I;

      ( rng I) = ( Image (I -functor (C,T))) by Def12;

      hence thesis;

    end;

    definition

      let C be Category;

      let I be Indexing of C;

      let m be Morphism of C;

      :: INDEX_1:def13

      func I . m -> Functor of ((I `1 ) . ( dom m)), ((I `1 ) . ( cod m)) equals ((I `2 ) . m);

      coherence

      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 thesis by FUNCT_1: 12;

      end;

    end

    definition

      let C be Category;

      let I be coIndexing of C;

      let m be Morphism of C;

      :: INDEX_1:def14

      func I . m -> Functor of ((I `1 ) . ( cod m)), ((I `1 ) . ( dom m)) equals ((I `2 ) . m);

      coherence

      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 thesis by FUNCT_1: 12;

      end;

    end

     Lm4:

    now

      let C,D be Category;

      set F = (the carrier of C --> D), G = (the carrier' of C --> ( id D));

      set H = [F, G];

      let m be Morphism of C;

      ( dom ((H `1 ) * the Source of C)) = the carrier' of C by PARTFUN1:def 2;

      

      then

       A1: (((H `1 ) * the Source of C) . m) = ((H `1 ) . (the Source of C . m)) by FUNCT_1: 12

      .= (F . (the Source of C . m))

      .= D;

      ( dom ((H `1 ) * the Target of C)) = the carrier' of C by PARTFUN1:def 2;

      

      then

       A2: (((H `1 ) * the Target of C) . m) = ((H `1 ) . (the Target of C . m)) by FUNCT_1: 12

      .= (F . (the Target of C . m))

      .= D;

      thus ((H `2 ) . m) is Functor of (((H `1 ) * the Source of C) . m), (((H `1 ) * the Target of C) . m) by A1, A2;

    end;

     Lm5:

    now

      let C,D be Category;

      set F = (the carrier of C --> D), G = (the carrier' of C --> ( id D));

      set H = [F, G];

      let m be Morphism of C;

      ( dom ((H `1 ) * the Source of C)) = the carrier' of C by PARTFUN1:def 2;

      

      then

       A1: (((H `1 ) * the Source of C) . m) = ((H `1 ) . (the Source of C . m)) by FUNCT_1: 12

      .= (F . (the Source of C . m))

      .= D;

      ( dom ((H `1 ) * the Target of C)) = the carrier' of C by PARTFUN1:def 2;

      

      then

       A2: (((H `1 ) * the Target of C) . m) = ((H `1 ) . (the Target of C . m)) by FUNCT_1: 12

      .= (F . (the Target of C . m))

      .= D;

      thus ((H `2 ) . m) is Functor of (((H `1 ) * the Target of C) . m), (((H `1 ) * the Source of C) . m) by A1, A2;

    end;

    theorem :: INDEX_1:15

    for C,D be 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;

      set H = [(the carrier of C --> D), (the carrier' of C --> ( id D))], I = H;

      

       A1: for a be Object of C holds ((H `2 ) . ( id a)) = ( id ((H `1 ) . a));

      for m be Morphism of C holds ((H `2 ) . m) is Functor of (((H `1 ) * the Source of C) . m), (((H `1 ) * the Target of C) . m) by Lm4;

      then (H `2 ) is ManySortedFunctor of ((H `1 ) * the Source of C), ((H `1 ) * the Target of C) by Def7;

      then

      reconsider H as Indexing of the Source of C, the Target of C by Def8;

      for m1,m2 be Morphism of C st ( dom m2) = ( cod m1) holds ((H `2 ) . (m2 (*) m1)) = (((H `2 ) . m2) * ((H `2 ) . m1)) by FUNCT_2: 17;

      hence I is Indexing of C by A1, Th6;

      for m be 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 as Indexing of the Target of C, the Source of C by Def8;

      for m1,m2 be Morphism of C st ( dom m2) = ( cod m1) holds ((H `2 ) . (m2 (*) m1)) = (((H `2 ) . m1) * ((H `2 ) . m2)) by FUNCT_2: 17;

      hence thesis by A1, Th7;

    end;

    begin

    registration

      let C be Category, D be Categorial Category;

      let F be Functor of C, D;

      cluster ( Obj F) -> Category-yielding;

      coherence

      proof

        let x be set;

        assume x in ( dom ( Obj F));

        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 thesis by CAT_5: 12;

      end;

    end

    theorem :: INDEX_1:16

    

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

    proof

      let C be Category, D be Categorial Category, F be Functor of C, D;

      set I = [( Obj F), ( pr2 F)];

      

       A1: ( dom F) = the carrier' of C by FUNCT_2:def 1;

      ( dom ( Obj F)) = the carrier of C by FUNCT_2:def 1;

      then

       A2: ( Obj F) is ManySortedSet of the carrier of C by PARTFUN1:def 2;

      

       A3: (I `2 ) = ( pr2 F);

      

       A4: ( dom ( pr2 F)) = ( dom F) by MCART_1:def 13;

      then ( pr2 F) is ManySortedSet of the carrier' of C by A1, PARTFUN1:def 2, RELAT_1:def 18;

      then

      reconsider I as ManySortedSet of the carrier of C, the carrier' of C by A2, Def4;

      ( pr2 F) is Function-yielding

      proof

        let x be object;

        assume x in ( dom ( pr2 F));

        then

        reconsider x as Morphism of C by A1, MCART_1:def 13;

        reconsider m = (F . x) as Morphism of D;

        (( pr2 F) . x) = (m `2 ) by A1, MCART_1:def 13;

        hence thesis;

      end;

      then

      reconsider FF = ( pr2 F) as ManySortedFunction of the carrier' of C by A4, A1, PARTFUN1:def 2, RELAT_1:def 18;

      (I `1 ) is Category-yielding;

      then

      reconsider 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;

        reconsider x = (F . m) as Morphism of D;

        

         A5: (x `11 ) = ( dom (F . m)) by CAT_5: 13;

        (x `12 ) = ( cod (F . m)) by CAT_5: 13;

        then

        consider f be Functor of (x `11 ), (x `12 ) such that

         A6: (F . m) = [ [(x `11 ), (x `12 )], f] by A5, CAT_5:def 6;

        

         A7: ((( Obj F) * the Source of C) . m) = (( Obj F) . ( dom m)) by FUNCT_2: 15

        .= ( dom (F . m)) by CAT_1: 69;

        

         A8: ((( 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 A1, MCART_1:def 13

        .= f by A6;

        hence thesis by A5, A7, A8, CAT_5: 13;

      end;

      then

      reconsider I as Indexing of the Source of C, the Target of C by A3, Def8;

      

       A9: ( dom F) = the carrier' of C by FUNCT_2:def 1;

       A10:

      now

        let m1,m2 be Morphism of C;

        assume

         A11: ( dom m2) = ( cod m1);

        set h1 = (F . m1), h2 = (F . m2);

        

         A12: ( dom h2) = (F . ( dom m2)) by CAT_1: 72

        .= ( cod h1) by A11, CAT_1: 72;

        

         A13: ( dom h2) = (h2 `11 ) by CAT_5: 13;

        ( cod h2) = (h2 `12 ) by CAT_5: 13;

        then

        consider f2 be Functor of (h2 `11 ), (h2 `12 ) such that

         A14: h2 = [ [(h2 `11 ), (h2 `12 )], f2] by A13, CAT_5:def 6;

        

         A15: ( cod h1) = (h1 `12 ) by CAT_5: 13;

        ( dom h1) = (h1 `11 ) by CAT_5: 13;

        then

        consider f1 be Functor of (h1 `11 ), (h1 `12 ) such that

         A16: h1 = [ [(h1 `11 ), (h1 `12 )], f1] by A15, CAT_5:def 6;

        

        thus ((I `2 ) . (m2 (*) m1)) = ((F . (m2 (*) m1)) `2 ) by A9, MCART_1:def 13

        .= ((h2 (*) h1) `2 ) by A11, CAT_1: 64

        .= ( [ [(h1 `11 ), (h2 `12 )], (f2 * f1)] `2 ) by A13, A15, A14, A16, A12, CAT_5:def 6

        .= (f2 * f1)

        .= ((h2 `2 ) * f1) by A14

        .= ((h2 `2 ) * (h1 `2 )) by A16

        .= (((I `2 ) . m2) * (h1 `2 )) by A9, MCART_1:def 13

        .= (((I `2 ) . m2) * ((I `2 ) . m1)) by A9, MCART_1:def 13;

      end;

      now

        let a be Object of C;

        reconsider i = (( Obj F) . a) as Object of D;

        

        thus ((I `2 ) . ( id a)) = ((F . ( id a) qua Morphism of C) `2 ) by A9, MCART_1:def 13

        .= (( id i) qua Morphism of D `2 ) by CAT_1: 68

        .= ( [ [((I `1 ) . a), ((I `1 ) . a)], ( id ((I `1 ) . a))] `2 ) by CAT_5:def 6

        .= ( id ((I `1 ) . a));

      end;

      hence thesis by A10, Th6;

    end;

    definition

      let C be Category;

      let D be Categorial Category;

      let F be Functor of C, D;

      :: INDEX_1:def15

      func F -indexing_of C -> Indexing of C equals [( Obj F), ( pr2 F)];

      coherence by Th16;

    end

    theorem :: INDEX_1:17

    for C be Category, D be Categorial Category, F be Functor of C, D holds D is TargetCat of (F -indexing_of C)

    proof

      let C be Category, D be Categorial Category, F be Functor of C, D;

      set I = (F -indexing_of C);

      thus for a be Object of C holds ((I `1 ) . a) is Object of D by FUNCT_2: 5;

      let b be Morphism of C;

      set h = (F . b);

      

       A1: ( dom h) = (h `11 ) by CAT_5: 13;

      ( cod h) = (h `12 ) by CAT_5: 13;

      then

      consider f be Functor of (h `11 ), (h `12 ) such that

       A2: h = [ [(h `11 ), (h `12 )], f] by A1, CAT_5:def 6;

      

       A3: ( cod h) = (( Obj F) . ( cod b)) by CAT_1: 69

      .= (( Obj F) . (the Target of C . b));

      

       A4: ( dom h) = (( Obj F) . ( dom b)) by CAT_1: 69

      .= (( Obj F) . (the Source of C . b));

      (I `2 ) = ( pr2 F) & ( dom F) = the carrier' of C by FUNCT_2:def 1;

      

      then ((I `2 ) . b) = (h `2 ) by MCART_1:def 13

      .= f by A2;

      hence thesis by A1, A2, A4, A3, CAT_5: 13;

    end;

    theorem :: INDEX_1:18

    

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

    proof

      let C be Category, D be Categorial Category, F be Functor of C, D;

      set I = (F -indexing_of C);

      let T be TargetCat of I;

      

       A1: ( dom F) = the carrier' of C by FUNCT_2:def 1;

       A2:

      now

        let x be object;

        assume x in the carrier' of C;

        then

        reconsider f = x as Morphism of C;

        set h = (F . f);

        

         A3: ( dom h) = (( Obj F) . ( dom f)) & ( cod h) = (( Obj F) . ( cod f)) by CAT_1: 69;

        

         A4: ( dom h) = (h `11 ) & ( cod h) = (h `12 ) by CAT_5: 13;

        then

        consider g be Functor of (h `11 ), (h `12 ) such that

         A5: h = [ [(h `11 ), (h `12 )], g] by CAT_5:def 6;

        ((I `2 ) . f) = (h `2 ) by A1, MCART_1:def 13

        .= g by A5;

        hence (F . x) = ((I -functor (C,T)) . x) by A4, A5, A3, Def11;

      end;

      thus thesis by A2;

    end;

    theorem :: INDEX_1:19

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

    theorem :: INDEX_1:20

    

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

    proof

      let C be Category, I be Indexing of C;

      let T be TargetCat of I;

      

       A1: ( dom (I -functor (C,T))) = the carrier' of C by FUNCT_2:def 1;

       A2:

      now

        let x be object;

        assume x in the carrier' of C;

        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);

        hence (( pr2 (I -functor (C,T))) . x) = ((I `2 ) . x) by A1, MCART_1:def 13;

      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 thesis by A1, A2;

    end;

    theorem :: INDEX_1:21

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

    proof

      let C be Category, I be Indexing of C;

      let T be TargetCat of I;

      set F = (I -functor (C,T));

      

       A1: ex f be ManySortedSet of the carrier of C, g be ManySortedSet of the carrier' of C st I = [f, g] by Def4;

      

      thus (F -indexing_of C) = [(I `1 ), ( pr2 F)] by Lm3

      .= [(I `1 ), (I `2 )] by Th20

      .= I by A1;

    end;

    begin

     Lm6:

    now

      let c,d be Category, e be Subcategory of d;

      let f be Functor of c, e;

      (( incl e) * f) = (( id e) * f) by CAT_2:def 5

      .= f by FUNCT_2: 17;

      hence f is Functor of c, d;

    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;

      :: INDEX_1:def16

      func I * F -> Indexing of C means

      : Def16: for F9 be Functor of C, E st F9 = F holds it = (((I -functor (E,( rng I))) * F9) -indexing_of C);

      existence

      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 as Functor of C, E by Lm6;

        take (((I -functor (E,( rng I))) * G) -indexing_of C);

        thus thesis;

      end;

      uniqueness

      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 such that

         A2: for F9 be Functor of C, E st F9 = F holds J1 = (((I -functor (E,( rng I))) * F9) -indexing_of C) and

         A3: for F9 be Functor of C, E st F9 = F holds J2 = (((I -functor (E,( rng I))) * F9) -indexing_of C);

        reconsider G as Functor of C, E by Lm6;

        

        thus J1 = (((I -functor (E,( rng I))) * G) -indexing_of C) by A2

        .= J2 by A3;

      end;

    end

    theorem :: INDEX_1:22

    

     Th22: for C,D1,D2,E be Category, I be Indexing of E holds for F be Functor of C, D1 holds for G be 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, I be Indexing of E;

      let F be Functor of C, D1, G be Functor of C, D2;

      assume that

       A1: ( Image F) is Subcategory of E and

       A2: ( Image G) is Subcategory of E and

       A3: F = G;

      reconsider F9 = F as Functor of C, ( Image F) by CAT_5: 8;

      reconsider F9 as Functor of C, E by A1, Lm6;

      (I * F) = (((I -functor (E,( rng I))) * F9) -indexing_of C) by A1, Def16;

      hence thesis by A2, A3, Def16;

    end;

    theorem :: INDEX_1:23

    

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

    proof

      let C,D be Category;

      let F be Functor of C, D;

      let I be Indexing of D;

      let T be TargetCat of I;

      ( 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 thesis by A1, Th2;

    end;

    theorem :: INDEX_1:24

    

     Th24: for C,D be Category, F be Functor of C, D, I be Indexing of D holds for T be TargetCat of I holds T is TargetCat of (I * F)

    proof

      let C,D be Category;

      let F be Functor of C, D;

      let I be Indexing of D;

      let T be TargetCat of I;

      set T9 = the TargetCat of (I * F);

      ( rng (I * F)) = ( Image ((I * F) -functor (C,T9))) & (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 thesis by Th14;

    end;

    theorem :: INDEX_1:25

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

    proof

      let C,D be Category;

      let F be Functor of C, D;

      let I be Indexing of D;

      let T be TargetCat of I;

      T is TargetCat of (I * F) by Th24;

      hence thesis by Th14;

    end;

    theorem :: INDEX_1:26

    

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

    proof

      let C,D,E be Category;

      let F be Functor of C, D;

      let G be Functor of D, E;

      let I be Indexing of E;

      set T = ( rng I);

      reconsider T9 = T as TargetCat of (I * G) by Th24;

      (I * G) = (((I -functor (E,T)) * G) -indexing_of D) by Th23;

      then ((I * G) -functor (D,T9)) = ((I -functor (E,T)) * G) by Th18;

      

      hence ((I * G) * F) = ((((I -functor (E,T)) * G) * F) -indexing_of C) by Th23

      .= (((I -functor (E,T)) * (G * F)) -indexing_of C) by RELAT_1: 36

      .= (I * (G * F)) by Th23;

    end;

    definition

      let C be Category;

      let I be Indexing of C;

      let D be Categorial Category;

      let E be Categorial Category;

      let F be Functor of D, E;

      :: INDEX_1:def17

      func F * I -> Indexing of C means

      : Def17: for T be TargetCat of I, G be Functor of T, E st T = D & G = F holds it = ((G * (I -functor (C,T))) -indexing_of C);

      existence

      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);

        thus thesis;

      end;

      uniqueness

      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;

        assume

         A2: not thesis;

        then J1 = ((G * (I -functor (C,T))) -indexing_of C);

        hence thesis by A2;

      end;

    end

    theorem :: INDEX_1:27

    

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

    proof

      let C be Category;

      let I be Indexing of C;

      let T be TargetCat of I, D,E be Categorial Category;

      let F be Functor of T, D;

      let G be Functor of T, E;

      assume

       A1: F = G;

      

      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;

    end;

    theorem :: INDEX_1:28

    

     Th28: for C be Category, I be Indexing of C holds for T be TargetCat of I, D be Categorial Category holds for F be Functor of T, D holds ( Image F) is TargetCat of (F * I)

    proof

      let C be Category;

      let I be Indexing of C;

      let T be TargetCat of I, D be Categorial Category;

      let F be Functor of T, D;

      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,T9))) 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 thesis by Th14;

    end;

    theorem :: INDEX_1:29

    

     Th29: for C be Category, I be Indexing of C holds for T be TargetCat of I, D be Categorial Category holds for F be Functor of T, D holds D is TargetCat of (F * I)

    proof

      let C be Category;

      let I be Indexing of C;

      let T be TargetCat of I, D be Categorial Category;

      let F be Functor of T, D;

      ( 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 thesis by Th14;

    end;

    theorem :: INDEX_1:30

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

    proof

      let C be Category;

      let I be Indexing of C;

      let T be TargetCat of I, D be Categorial Category;

      let F be Functor of T, D;

      ( Image F) is TargetCat of (F * I) by Th28;

      hence thesis by Th14;

    end;

    theorem :: INDEX_1:31

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

    proof

      let C be Category;

      let I be Indexing of C;

      let T be TargetCat of I;

      let D,E be Categorial Category;

      let F be Functor of T, D;

      reconsider D9 = D as TargetCat of (F * I) by Th29;

      let G be Functor of D, E;

      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;

    end;

    definition

      let C,D be Category;

      let I1 be Indexing of C;

      let I2 be Indexing of D;

      :: INDEX_1:def18

      func I2 * I1 -> Indexing of C equals (I2 * (I1 -functor (C,( rng I1))));

      correctness ;

    end

    theorem :: INDEX_1:32

    

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

    proof

      let C be Category, D be Categorial Category;

      let I1 be Indexing of C;

      let I2 be Indexing of D;

      let T be TargetCat of I1;

      assume D is TargetCat of I1;

      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 thesis by A1, Th11, Th22;

    end;

    theorem :: INDEX_1:33

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

    proof

      let C be Category, D be Categorial Category;

      let I1 be Indexing of C;

      let I2 be Indexing of D;

      let T be TargetCat of I2;

      assume D is TargetCat of 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;

    end;

    theorem :: INDEX_1:34

    

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

    proof

      let C,D be Category, F be Functor of C, D, I be Indexing of D;

      let T be TargetCat of I;

      reconsider T9 = T as TargetCat of (I * F) by Th24;

      let E be Categorial Category, G be Functor of T, E;

      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;

    end;

    theorem :: INDEX_1:35

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

    proof

      let C be Category, I be Indexing of C;

      let T be TargetCat of I;

      let D be Categorial Category, F be Functor of T, D;

      let J be Indexing of D;

      

       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;

    end;

    theorem :: INDEX_1:36

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

    proof

      let C be Category, I be Indexing of C;

      let T1 be TargetCat of I;

      let J be Indexing of T1;

      let T2 be TargetCat of J;

      let D be Categorial Category, F be Functor of T2, D;

      

      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;

    end;

    theorem :: INDEX_1:37

    

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

    proof

      let C,D be Category, F be Functor of C, D, I be Indexing of D;

      let T be TargetCat of I, J be Indexing of T;

      

       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;

    end;

    theorem :: INDEX_1:38

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

    proof

      let C be Category, I be Indexing of C;

      let D be TargetCat of I, J be Indexing of D;

      let E be TargetCat of J, K be Indexing of E;

      

      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;

    end;

    theorem :: INDEX_1:39

    for C be Category holds ( IdMap C) = ( IdMap (C opp )) by Lm2;