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