:: CAT_2 semantic presentation begin theorem :: CAT_2:1 canceled; theorem :: CAT_2:2 canceled; theorem :: CAT_2:3 canceled; theorem :: CAT_2:4 canceled; definition let B, C be Category; let c be Object of C; funcB --> c -> Functor of B,C equals :: CAT_2:def 1 the carrier' of B --> (id c); coherence the carrier' of B --> (id c) is Functor of B,C proof reconsider T = the carrier' of B --> (id c) as Function of the carrier' of B, the carrier' of C ; now__::_thesis:_(_(_for_b_being_Object_of_B_ex_d_being_Object_of_C_st_T_._(id_b)_=_id_d_)_&_(_for_f_being_Morphism_of_B_holds_ (_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_B_st_dom_g_=_cod_f_holds_ T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_) thus for b being Object of B ex d being Object of C st T . (id b) = id d by FUNCOP_1:7; ::_thesis: ( ( for f being Morphism of B holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) ) thus for f being Morphism of B holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of B st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) proof let f be Morphism of B; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) T . (id (cod f)) = id c by FUNCOP_1:7; then A1: T . (id (cod f)) = id (cod (id c)) ; T . (id (dom f)) = id c by FUNCOP_1:7; then T . (id (dom f)) = id (dom (id c)) ; hence ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A1, FUNCOP_1:7; ::_thesis: verum end; let f, g be Morphism of B; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) ) assume dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f) Hom (c,c) <> {} ; then A2: ( T . f = id c & (id c) * (id c) = (id c) (*) (id c) ) by CAT_1:def_13, FUNCOP_1:7; ( T . (g (*) f) = id c & T . g = id c ) by FUNCOP_1:7; hence T . (g (*) f) = (T . g) (*) (T . f) by A2; ::_thesis: verum end; hence the carrier' of B --> (id c) is Functor of B,C by CAT_1:61; ::_thesis: verum end; end; :: deftheorem defines --> CAT_2:def_1_:_ for B, C being Category for c being Object of C holds B --> c = the carrier' of B --> (id c); theorem :: CAT_2:5 for C, B being Category for c being Object of C for b being Object of B holds (Obj (B --> c)) . b = c proof let C, B be Category; ::_thesis: for c being Object of C for b being Object of B holds (Obj (B --> c)) . b = c let c be Object of C; ::_thesis: for b being Object of B holds (Obj (B --> c)) . b = c let b be Object of B; ::_thesis: (Obj (B --> c)) . b = c (B --> c) . (id b) = id c by FUNCOP_1:7; hence (Obj (B --> c)) . b = c by CAT_1:67; ::_thesis: verum end; definition let C, D be Category; func Funct (C,D) -> set means :Def2: :: CAT_2:def 2 for x being set holds ( x in it iff x is Functor of C,D ); existence ex b1 being set st for x being set holds ( x in b1 iff x is Functor of C,D ) proof defpred S1[ set ] means \$1 is Functor of C,D; consider F being set such that A1: for x being set holds ( x in F iff ( x in Funcs ( the carrier' of C, the carrier' of D) & S1[x] ) ) from XBOOLE_0:sch_1(); take F ; ::_thesis: for x being set holds ( x in F iff x is Functor of C,D ) let x be set ; ::_thesis: ( x in F iff x is Functor of C,D ) thus ( x in F implies x is Functor of C,D ) by A1; ::_thesis: ( x is Functor of C,D implies x in F ) assume A2: x is Functor of C,D ; ::_thesis: x in F then x in Funcs ( the carrier' of C, the carrier' of D) by FUNCT_2:8; hence x in F by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is Functor of C,D ) ) & ( for x being set holds ( x in b2 iff x is Functor of C,D ) ) holds b1 = b2 proof let F1, F2 be set ; ::_thesis: ( ( for x being set holds ( x in F1 iff x is Functor of C,D ) ) & ( for x being set holds ( x in F2 iff x is Functor of C,D ) ) implies F1 = F2 ) assume that A3: for x being set holds ( x in F1 iff x is Functor of C,D ) and A4: for x being set holds ( x in F2 iff x is Functor of C,D ) ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_set_holds_ (_x_in_F1_iff_x_in_F2_) let x be set ; ::_thesis: ( x in F1 iff x in F2 ) ( x in F1 iff x is Functor of C,D ) by A3; hence ( x in F1 iff x in F2 ) by A4; ::_thesis: verum end; hence F1 = F2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def2 defines Funct CAT_2:def_2_:_ for C, D being Category for b3 being set holds ( b3 = Funct (C,D) iff for x being set holds ( x in b3 iff x is Functor of C,D ) ); registration let C, D be Category; cluster Funct (C,D) -> non empty ; coherence not Funct (C,D) is empty proof set x = the Functor of C,D; the Functor of C,D in Funct (C,D) by Def2; hence not Funct (C,D) is empty ; ::_thesis: verum end; end; definition let C, D be Category; mode FUNCTOR-DOMAIN of C,D -> non empty set means :Def3: :: CAT_2:def 3 for x being Element of it holds x is Functor of C,D; existence ex b1 being non empty set st for x being Element of b1 holds x is Functor of C,D proof take Funct (C,D) ; ::_thesis: for x being Element of Funct (C,D) holds x is Functor of C,D thus for x being Element of Funct (C,D) holds x is Functor of C,D by Def2; ::_thesis: verum end; end; :: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def_3_:_ for C, D being Category for b3 being non empty set holds ( b3 is FUNCTOR-DOMAIN of C,D iff for x being Element of b3 holds x is Functor of C,D ); definition let C, D be Category; let F be FUNCTOR-DOMAIN of C,D; :: original: Element redefine mode Element of F -> Functor of C,D; coherence for b1 being Element of F holds b1 is Functor of C,D by Def3; end; definition let A be non empty set ; let C, D be Category; let F be FUNCTOR-DOMAIN of C,D; let T be Function of A,F; let x be Element of A; :: original: . redefine funcT . x -> Element of F; coherence T . x is Element of F proof thus T . x is Element of F ; ::_thesis: verum end; end; definition let C, D be Category; :: original: Funct redefine func Funct (C,D) -> FUNCTOR-DOMAIN of C,D; coherence Funct (C,D) is FUNCTOR-DOMAIN of C,D proof let x be Element of Funct (C,D); :: according to CAT_2:def_3 ::_thesis: x is Functor of C,D thus x is Functor of C,D by Def2; ::_thesis: verum end; end; definition let C be Category; mode Subcategory of C -> Category means :Def4: :: CAT_2:def 4 ( the carrier of it c= the carrier of C & ( for a, b being Object of it for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of it c= the Comp of C & ( for a being Object of it for a9 being Object of C st a = a9 holds id a = id a9 ) ); existence ex b1 being Category st ( the carrier of b1 c= the carrier of C & ( for a, b being Object of b1 for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of b1 c= the Comp of C & ( for a being Object of b1 for a9 being Object of C st a = a9 holds id a = id a9 ) ) proof take C ; ::_thesis: ( the carrier of C c= the carrier of C & ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds id a = id a9 ) ) thus ( the carrier of C c= the carrier of C & ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds id a = id a9 ) ) ; ::_thesis: verum end; end; :: deftheorem Def4 defines Subcategory CAT_2:def_4_:_ for C, b2 being Category holds ( b2 is Subcategory of C iff ( the carrier of b2 c= the carrier of C & ( for a, b being Object of b2 for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of b2 c= the Comp of C & ( for a being Object of b2 for a9 being Object of C st a = a9 holds id a = id a9 ) ) ); registration let C be Category; cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities for Subcategory of C; existence ex b1 being Subcategory of C st b1 is strict proof set c = the Object of C; set E = 1Cat ( the Object of C,(id the Object of C)); now__::_thesis:_(_the_carrier_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C)))_c=_the_carrier_of_C_&_(_for_a,_b_being_Object_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C))) for_a9,_b9_being_Object_of_C_st_a_=_a9_&_b_=_b9_holds_ Hom_(a,b)_c=_Hom_(a9,b9)_)_&_the_Comp_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C)))_c=_the_Comp_of_C_&_(_for_a_being_Object_of_(1Cat_(_the_Object_of_C,(id_the_Object_of_C))) for_a9_being_Object_of_C_st_a_=_a9_holds_ id_a_=_id_a9_)_) thus the carrier of (1Cat ( the Object of C,(id the Object of C))) c= the carrier of C ::_thesis: ( ( for a, b being Object of (1Cat ( the Object of C,(id the Object of C))) for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C))) for a9 being Object of C st a = a9 holds id a = id a9 ) ) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of (1Cat ( the Object of C,(id the Object of C))) or a in the carrier of C ) assume a in the carrier of (1Cat ( the Object of C,(id the Object of C))) ; ::_thesis: a in the carrier of C then a = the Object of C by TARSKI:def_1; hence a in the carrier of C ; ::_thesis: verum end; thus for a, b being Object of (1Cat ( the Object of C,(id the Object of C))) for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ::_thesis: ( the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C))) for a9 being Object of C st a = a9 holds id a = id a9 ) ) proof let a, b be Object of (1Cat ( the Object of C,(id the Object of C))); ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) ) assume ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) c= Hom (a9,b9) then A1: ( a9 = the Object of C & b9 = the Object of C ) by TARSKI:def_1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) ) assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then x = id the Object of C by TARSKI:def_1; hence x in Hom (a9,b9) by A1, CAT_1:27; ::_thesis: verum end; thus the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C ::_thesis: for a being Object of (1Cat ( the Object of C,(id the Object of C))) for a9 being Object of C st a = a9 holds id a = id a9 proof reconsider i = id the Object of C as Morphism of C ; A2: Hom ( the Object of C, the Object of C) <> {} ; A3: ( dom (id the Object of C) = the Object of C & cod (id the Object of C) = the Object of C ) ; then A4: [(id the Object of C),(id the Object of C)] in dom the Comp of C by CAT_1:15; the Comp of (1Cat ( the Object of C,(id the Object of C))) = ((id the Object of C),(id the Object of C)) .--> ((id the Object of C) * (id the Object of C)) .= ((id the Object of C),(id the Object of C)) .--> ((id the Object of C) (*) i) by A2, CAT_1:def_13 .= [(id the Object of C),(id the Object of C)] .--> ( the Comp of C . ((id the Object of C),(id the Object of C))) by A3, CAT_1:16 ; hence the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C by A4, FUNCT_4:7; ::_thesis: verum end; let a be Object of (1Cat ( the Object of C,(id the Object of C))); ::_thesis: for a9 being Object of C st a = a9 holds id a = id a9 let a9 be Object of C; ::_thesis: ( a = a9 implies id a = id a9 ) assume a = a9 ; ::_thesis: id a = id a9 then a9 = the Object of C by TARSKI:def_1; hence id a = id a9 by TARSKI:def_1; ::_thesis: verum end; then 1Cat ( the Object of C,(id the Object of C)) is Subcategory of C by Def4; hence ex b1 being Subcategory of C st b1 is strict ; ::_thesis: verum end; end; theorem Th6: :: CAT_2:6 for C being Category for E being Subcategory of C for e being Object of E holds e is Object of C proof let C be Category; ::_thesis: for E being Subcategory of C for e being Object of E holds e is Object of C let E be Subcategory of C; ::_thesis: for e being Object of E holds e is Object of C let e be Object of E; ::_thesis: e is Object of C ( e in the carrier of E & the carrier of E c= the carrier of C ) by Def4; hence e is Object of C ; ::_thesis: verum end; theorem Th7: :: CAT_2:7 for C being Category for E being Subcategory of C holds the carrier' of E c= the carrier' of C proof let C be Category; ::_thesis: for E being Subcategory of C holds the carrier' of E c= the carrier' of C let E be Subcategory of C; ::_thesis: the carrier' of E c= the carrier' of C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of E or x in the carrier' of C ) assume x in the carrier' of E ; ::_thesis: x in the carrier' of C then reconsider f = x as Morphism of E ; set a = dom f; set b = cod f; reconsider a9 = dom f, b9 = cod f as Object of C by Th6; ( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4; then ( f in Hom (a9,b9) & Hom (a9,b9) <> {} ) ; hence x in the carrier' of C ; ::_thesis: verum end; theorem Th8: :: CAT_2:8 for C being Category for E being Subcategory of C for f being Morphism of E holds f is Morphism of C proof let C be Category; ::_thesis: for E being Subcategory of C for f being Morphism of E holds f is Morphism of C let E be Subcategory of C; ::_thesis: for f being Morphism of E holds f is Morphism of C let f be Morphism of E; ::_thesis: f is Morphism of C ( f in the carrier' of E & the carrier' of E c= the carrier' of C ) by Th7; hence f is Morphism of C ; ::_thesis: verum end; theorem Th9: :: CAT_2:9 for C being Category for E being Subcategory of C for f being Morphism of E for f9 being Morphism of C st f = f9 holds ( dom f = dom f9 & cod f = cod f9 ) proof let C be Category; ::_thesis: for E being Subcategory of C for f being Morphism of E for f9 being Morphism of C st f = f9 holds ( dom f = dom f9 & cod f = cod f9 ) let E be Subcategory of C; ::_thesis: for f being Morphism of E for f9 being Morphism of C st f = f9 holds ( dom f = dom f9 & cod f = cod f9 ) let f be Morphism of E; ::_thesis: for f9 being Morphism of C st f = f9 holds ( dom f = dom f9 & cod f = cod f9 ) let f9 be Morphism of C; ::_thesis: ( f = f9 implies ( dom f = dom f9 & cod f = cod f9 ) ) assume A1: f = f9 ; ::_thesis: ( dom f = dom f9 & cod f = cod f9 ) set a = dom f; set b = cod f; reconsider a9 = dom f, b9 = cod f as Object of C by Th6; ( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4; hence ( dom f = dom f9 & cod f = cod f9 ) by A1, CAT_1:1; ::_thesis: verum end; theorem :: CAT_2:10 for C being Category for E being Subcategory of C for a, b being Object of E for a9, b9 being Object of C for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds f is Morphism of a9,b9 proof let C be Category; ::_thesis: for E being Subcategory of C for a, b being Object of E for a9, b9 being Object of C for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds f is Morphism of a9,b9 let E be Subcategory of C; ::_thesis: for a, b being Object of E for a9, b9 being Object of C for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds f is Morphism of a9,b9 let a, b be Object of E; ::_thesis: for a9, b9 being Object of C for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds f is Morphism of a9,b9 let a9, b9 be Object of C; ::_thesis: for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds f is Morphism of a9,b9 let f be Morphism of a,b; ::_thesis: ( a = a9 & b = b9 & Hom (a,b) <> {} implies f is Morphism of a9,b9 ) assume ( a = a9 & b = b9 & Hom (a,b) <> {} ) ; ::_thesis: f is Morphism of a9,b9 then ( f in Hom (a,b) & Hom (a,b) c= Hom (a9,b9) ) by Def4, CAT_1:def_5; then ( f in Hom (a9,b9) & Hom (a9,b9) <> {} ) ; hence f is Morphism of a9,b9 by CAT_1:def_5; ::_thesis: verum end; theorem Th11: :: CAT_2:11 for C being Category for E being Subcategory of C for f, g being Morphism of E for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds g (*) f = g9 (*) f9 proof let C be Category; ::_thesis: for E being Subcategory of C for f, g being Morphism of E for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds g (*) f = g9 (*) f9 let E be Subcategory of C; ::_thesis: for f, g being Morphism of E for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds g (*) f = g9 (*) f9 let f, g be Morphism of E; ::_thesis: for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds g (*) f = g9 (*) f9 let f9, g9 be Morphism of C; ::_thesis: ( f = f9 & g = g9 & dom g = cod f implies g (*) f = g9 (*) f9 ) assume that A1: ( f = f9 & g = g9 ) and A2: dom g = cod f ; ::_thesis: g (*) f = g9 (*) f9 ( dom g = dom g9 & cod f = cod f9 ) by A1, Th9; then A3: g9 (*) f9 = the Comp of C . (g9,f9) by A2, CAT_1:16; A4: the Comp of E c= the Comp of C by Def4; ( g (*) f = the Comp of E . (g,f) & [g,f] in dom the Comp of E ) by A2, CAT_1:15, CAT_1:16; hence g (*) f = g9 (*) f9 by A1, A3, A4, GRFUNC_1:2; ::_thesis: verum end; theorem Th12: :: CAT_2:12 for C being Category holds C is Subcategory of C proof let C be Category; ::_thesis: C is Subcategory of C thus the carrier of C c= the carrier of C ; :: according to CAT_2:def_4 ::_thesis: ( ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds id a = id a9 ) ) thus ( ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds id a = id a9 ) ) ; ::_thesis: verum end; theorem Th13: :: CAT_2:13 for C being Category for E being Subcategory of C holds id E is Functor of E,C proof let C be Category; ::_thesis: for E being Subcategory of C holds id E is Functor of E,C let E be Subcategory of C; ::_thesis: id E is Functor of E,C rng (id E) = the carrier' of E by RELAT_1:45; then rng (id E) c= the carrier' of C by Th7; then reconsider T = id E as Function of the carrier' of E, the carrier' of C by FUNCT_2:6; now__::_thesis:_(_(_for_e_being_Object_of_E_ex_c_being_Object_of_C_st_T_._(id_e)_=_id_c_)_&_(_for_f_being_Morphism_of_E_holds_ (_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_E_st_dom_g_=_cod_f_holds_ T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_) thus for e being Object of E ex c being Object of C st T . (id e) = id c ::_thesis: ( ( for f being Morphism of E holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of E st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) ) proof let e be Object of E; ::_thesis: ex c being Object of C st T . (id e) = id c reconsider c = e as Object of C by Th6; T . (id e) = id e by FUNCT_1:18 .= id c by Def4 ; hence ex c being Object of C st T . (id e) = id c ; ::_thesis: verum end; thus for f being Morphism of E holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of E st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) proof let f be Morphism of E; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) A1: T . (id (dom f)) = id (dom f) by FUNCT_1:18 .= id (dom ((id E) . f)) by FUNCT_1:18 ; A2: T . (id (cod f)) = id (cod f) by FUNCT_1:18 .= id (cod ((id E) . f)) by FUNCT_1:18 ; ( dom (T . f) = dom ((id E) . f) & cod (T . f) = cod ((id E) . f) ) by Th9; hence ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A1, A2, Def4; ::_thesis: verum end; let f, g be Morphism of E; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) ) A3: ( T . f = f & T . g = g ) by FUNCT_1:18; assume A4: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f) then T . (g (*) f) = ((id E) . g) (*) ((id E) . f) by CAT_1:64; hence T . (g (*) f) = (T . g) (*) (T . f) by A4, A3, Th11; ::_thesis: verum end; hence id E is Functor of E,C by CAT_1:61; ::_thesis: verum end; definition let C be Category; let E be Subcategory of C; func incl E -> Functor of E,C equals :: CAT_2:def 5 id E; coherence id E is Functor of E,C by Th13; end; :: deftheorem defines incl CAT_2:def_5_:_ for C being Category for E being Subcategory of C holds incl E = id E; theorem Th14: :: CAT_2:14 for C being Category for E being Subcategory of C for a being Object of E holds (Obj (incl E)) . a = a proof let C be Category; ::_thesis: for E being Subcategory of C for a being Object of E holds (Obj (incl E)) . a = a let E be Subcategory of C; ::_thesis: for a being Object of E holds (Obj (incl E)) . a = a let a be Object of E; ::_thesis: (Obj (incl E)) . a = a reconsider a9 = a as Object of C by Th6; id a9 = id a by Def4 .= (incl E) . (id a) by FUNCT_1:18 .= id ((Obj (incl E)) . a) by CAT_1:68 ; hence (Obj (incl E)) . a = a by CAT_1:59; ::_thesis: verum end; theorem :: CAT_2:15 for C being Category for E being Subcategory of C for a being Object of E holds (incl E) . a = a by Th14; theorem :: CAT_2:16 for C being Category for E being Subcategory of C holds incl E is faithful proof let C be Category; ::_thesis: for E being Subcategory of C holds incl E is faithful let E be Subcategory of C; ::_thesis: incl E is faithful let a, b be Object of E; :: according to CAT_1:def_27 ::_thesis: ( Hom (a,b) = {} or for b1, b2 being Morphism of a,b holds ( not (incl E) . b1 = (incl E) . b2 or b1 = b2 ) ) assume Hom (a,b) <> {} ; ::_thesis: for b1, b2 being Morphism of a,b holds ( not (incl E) . b1 = (incl E) . b2 or b1 = b2 ) let f1, f2 be Morphism of a,b; ::_thesis: ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 ) (incl E) . f1 = f1 by FUNCT_1:18; hence ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 ) by FUNCT_1:18; ::_thesis: verum end; theorem Th17: :: CAT_2:17 for C being Category for E being Subcategory of C holds ( incl E is full iff for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) ) proof let C be Category; ::_thesis: for E being Subcategory of C holds ( incl E is full iff for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) ) let E be Subcategory of C; ::_thesis: ( incl E is full iff for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) ) set T = incl E; thus ( incl E is full implies for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) ) ::_thesis: ( ( for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) ) implies incl E is full ) proof assume A1: for a, b being Object of E st Hom (((incl E) . a),((incl E) . b)) <> {} holds for g being Morphism of (incl E) . a,(incl E) . b holds ( Hom (a,b) <> {} & ex f being Morphism of a,b st g = (incl E) . f ) ; :: according to CAT_1:def_26 ::_thesis: for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) let a, b be Object of E; ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) ) assume A2: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Hom_(a,b)_implies_x_in_Hom_(a9,b9)_)_&_(_x_in_Hom_(a9,b9)_implies_x_in_Hom_(a,b)_)_) let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) ) Hom (a,b) c= Hom (a9,b9) by A2, Def4; hence ( x in Hom (a,b) implies x in Hom (a9,b9) ) ; ::_thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) ) assume A3: x in Hom (a9,b9) ; ::_thesis: x in Hom (a,b) A4: ( (incl E) . a = a9 & (incl E) . b = b9 ) by A2, Th14; then reconsider g = x as Morphism of (incl E) . a,(incl E) . b by A3, CAT_1:def_5; consider f being Morphism of a,b such that A5: g = (incl E) . f by A1, A4, A3; A6: g = f by A5, FUNCT_1:18; Hom (a,b) <> {} by A1, A4, A3; hence x in Hom (a,b) by A6, CAT_1:def_5; ::_thesis: verum end; hence Hom (a,b) = Hom (a9,b9) by TARSKI:1; ::_thesis: verum end; assume A7: for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) ; ::_thesis: incl E is full let a, b be Object of E; :: according to CAT_1:def_26 ::_thesis: ( Hom (((incl E) . a),((incl E) . b)) = {} or for b1 being Morphism of (incl E) . a,(incl E) . b holds ( not Hom (a,b) = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 ) ) assume A8: Hom (((incl E) . a),((incl E) . b)) <> {} ; ::_thesis: for b1 being Morphism of (incl E) . a,(incl E) . b holds ( not Hom (a,b) = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 ) let g be Morphism of (incl E) . a,(incl E) . b; ::_thesis: ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st g = (incl E) . b1 ) A9: g in Hom (((incl E) . a),((incl E) . b)) by A8, CAT_1:def_5; A10: ( a = (incl E) . a & b = (incl E) . b ) by Th14; hence Hom (a,b) <> {} by A7, A8; ::_thesis: ex b1 being Morphism of a,b st g = (incl E) . b1 Hom (a,b) = Hom (((incl E) . a),((incl E) . b)) by A7, A10; then reconsider f = g as Morphism of a,b by A9, CAT_1:def_5; take f ; ::_thesis: g = (incl E) . f thus g = (incl E) . f by FUNCT_1:18; ::_thesis: verum end; definition let D be Category; let C be Subcategory of D; attrC is full means :Def6: :: CAT_2:def 6 for c1, c2 being Object of C for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds Hom (c1,c2) = Hom (d1,d2); end; :: deftheorem Def6 defines full CAT_2:def_6_:_ for D being Category for C being Subcategory of D holds ( C is full iff for c1, c2 being Object of C for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds Hom (c1,c2) = Hom (d1,d2) ); registration let D be Category; cluster non empty non void V55() Category-like transitive associative reflexive with_identities full for Subcategory of D; existence ex b1 being Subcategory of D st b1 is full proof reconsider C = D as Subcategory of D by Th12; take C ; ::_thesis: C is full let c1, c2 be Object of C; :: according to CAT_2:def_6 ::_thesis: for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds Hom (c1,c2) = Hom (d1,d2) let d1, d2 be Object of D; ::_thesis: ( c1 = d1 & c2 = d2 implies Hom (c1,c2) = Hom (d1,d2) ) assume ( c1 = d1 & c2 = d2 ) ; ::_thesis: Hom (c1,c2) = Hom (d1,d2) hence Hom (c1,c2) = Hom (d1,d2) ; ::_thesis: verum end; end; theorem :: CAT_2:18 for C being Category for E being Subcategory of C holds ( E is full iff incl E is full ) proof let C be Category; ::_thesis: for E being Subcategory of C holds ( E is full iff incl E is full ) let E be Subcategory of C; ::_thesis: ( E is full iff incl E is full ) thus ( E is full implies incl E is full ) ::_thesis: ( incl E is full implies E is full ) proof assume E is full ; ::_thesis: incl E is full then for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) by Def6; hence incl E is full by Th17; ::_thesis: verum end; assume incl E is full ; ::_thesis: E is full hence for a, b being Object of E for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) by Th17; :: according to CAT_2:def_6 ::_thesis: verum end; theorem Th19: :: CAT_2:19 for C being Category for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C proof let C be Category; ::_thesis: for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C let O be non empty Subset of the carrier of C; ::_thesis: union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; set M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; A1: union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } c= the carrier' of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } or x in the carrier' of C ) assume x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; ::_thesis: x in the carrier' of C then consider X being set such that A2: x in X and A3: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def_4; ex a, b being Object of C st ( X = Hom (a,b) & a in O & b in O ) by A3; hence x in the carrier' of C by A2; ::_thesis: verum end; now__::_thesis:_ex_f_being_set_st_f_in_union__{__(Hom_(a,b))_where_a,_b_is_Object_of_C_:_(_a_in_O_&_b_in_O_)__}_ set a = the Element of O; reconsider a = the Element of O as Object of C ; ( id a in Hom (a,a) & Hom (a,a) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) by CAT_1:27; then id a in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def_4; hence ex f being set st f in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; ::_thesis: verum end; hence union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C by A1; ::_thesis: verum end; theorem Th20: :: CAT_2:20 for C being Category for O being non empty Subset of the carrier of C for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) proof let C be Category; ::_thesis: for O being non empty Subset of the carrier of C for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) let O be non empty Subset of the carrier of C; ::_thesis: for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; A1: dom the Source of C = the carrier' of C by FUNCT_2:def_1; let M be non empty set ; ::_thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) ) assume A2: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; ::_thesis: ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) A3: now__::_thesis:_for_f_being_Morphism_of_C_st_f_in_M_holds_ (_dom_f_in_O_&_cod_f_in_O_) let f be Morphism of C; ::_thesis: ( f in M implies ( dom f in O & cod f in O ) ) assume f in M ; ::_thesis: ( dom f in O & cod f in O ) then consider X being set such that A4: f in X and A5: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A2, TARSKI:def_4; ex a, b being Object of C st ( X = Hom (a,b) & a in O & b in O ) by A5; hence ( dom f in O & cod f in O ) by A4, CAT_1:1; ::_thesis: verum end; set d = the Source of C | M; set c = the Target of C | M; set p = the Comp of C || M; A6: dom the Target of C = the carrier' of C by FUNCT_2:def_1; A7: dom ( the Source of C | M) = (dom the Source of C) /\ M by RELAT_1:61; A8: rng ( the Source of C | M) c= O proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Source of C | M) or y in O ) assume y in rng ( the Source of C | M) ; ::_thesis: y in O then consider x being set such that A9: x in dom ( the Source of C | M) and A10: y = ( the Source of C | M) . x by FUNCT_1:def_3; reconsider f = x as Morphism of C by A1, A7, A9, XBOOLE_0:def_4; ( ( the Source of C | M) . f = dom f & f in M ) by A7, A9, FUNCT_1:47, XBOOLE_0:def_4; hence y in O by A3, A10; ::_thesis: verum end; A11: M is non empty Subset of the carrier' of C by A2, Th19; then A12: dom ( the Target of C | M) = M by A6, RELAT_1:62; A13: dom ( the Target of C | M) = (dom the Target of C) /\ M by RELAT_1:61; A14: rng ( the Target of C | M) c= O proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Target of C | M) or y in O ) assume y in rng ( the Target of C | M) ; ::_thesis: y in O then consider x being set such that A15: x in dom ( the Target of C | M) and A16: y = ( the Target of C | M) . x by FUNCT_1:def_3; reconsider f = x as Morphism of C by A6, A13, A15, XBOOLE_0:def_4; ( ( the Target of C | M) . f = cod f & f in M ) by A13, A15, FUNCT_1:47, XBOOLE_0:def_4; hence y in O by A3, A16; ::_thesis: verum end; dom ( the Source of C | M) = M by A1, A11, RELAT_1:62; hence ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O ) by A8, A14, A12, FUNCT_2:def_1, RELSET_1:4; ::_thesis: the Comp of C || M is PartFunc of [:M,M:],M A17: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61; A18: dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def_18; rng ( the Comp of C || M) c= M proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Comp of C || M) or y in M ) assume y in rng ( the Comp of C || M) ; ::_thesis: y in M then consider x being set such that A19: x in dom ( the Comp of C || M) and A20: y = ( the Comp of C || M) . x by FUNCT_1:def_3; A21: x in dom the Comp of C by A17, A19, XBOOLE_0:def_4; then consider g, f being Morphism of C such that A22: x = [g,f] by A18, DOMAIN_1:1; A23: [g,f] in [:M,M:] by A17, A19, A22, XBOOLE_0:def_4; then g in M by ZFMISC_1:87; then A24: cod g in O by A3; dom g = cod f by A21, A22, CAT_1:15; then A25: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by CAT_1:17; f in M by A23, ZFMISC_1:87; then dom f in O by A3; then A26: Hom ((dom (g (*) f)),(cod (g (*) f))) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A24, A25; A27: g (*) f in Hom ((dom (g (*) f)),(cod (g (*) f))) ; ( the Comp of C || M) . x = the Comp of C . (g,f) by A19, A22, FUNCT_1:47 .= g (*) f by A21, A22, CAT_1:def_1 ; hence y in M by A2, A20, A26, A27, TARSKI:def_4; ::_thesis: verum end; hence the Comp of C || M is PartFunc of [:M,M:],M by A17, RELSET_1:4, XBOOLE_1:17; ::_thesis: verum thus verum ; ::_thesis: verum end; registration let O, M be non empty set ; let d, c be Function of M,O; let p be PartFunc of [:M,M:],M; cluster CatStr(# O,M,d,c,p #) -> non empty non void ; coherence ( not CatStr(# O,M,d,c,p #) is void & not CatStr(# O,M,d,c,p #) is empty ) ; end; Lm1: for C being Category for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Category proof let C be Category; ::_thesis: for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Category let O be non empty Subset of the carrier of C; ::_thesis: for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Category let M be non empty set ; ::_thesis: for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Category let d, c be Function of M,O; ::_thesis: for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Category let p be PartFunc of [:M,M:],M; ::_thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Category let i be Function of O,M; ::_thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Category ) set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; assume that A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and A2: d = the Source of C | M and A3: c = the Target of C | M and A4: p = the Comp of C || M ; ::_thesis: CatStr(# O,M,d,c,p #) is Category set B = CatStr(# O,M,d,c,p #); A5: now__::_thesis:_for_f_being_Morphism_of_CatStr(#_O,M,d,c,p_#)_holds_f_is_Morphism_of_C let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: f is Morphism of C consider X being set such that A6: f in X and A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def_4; ex a, b being Object of C st ( X = Hom (a,b) & a in O & b in O ) by A7; hence f is Morphism of C by A6; ::_thesis: verum end; A8: for f, g being Morphism of CatStr(# O,M,d,c,p #) holds ( [g,f] in dom p iff d . g = c . f ) proof let f, g be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( [g,f] in dom p iff d . g = c . f ) reconsider gg = g, ff = f as Morphism of C by A5; A9: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49; thus ( [g,f] in dom p implies d . g = c . f ) ::_thesis: ( d . g = c . f implies [g,f] in dom p ) proof assume [g,f] in dom p ; ::_thesis: d . g = c . f then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61; then [gg,ff] in dom the Comp of C by XBOOLE_0:def_4; hence d . g = c . f by A9, CAT_1:def_6; ::_thesis: verum end; assume d . g = c . f ; ::_thesis: [g,f] in dom p then [g,f] in dom the Comp of C by A9, CAT_1:def_6; then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def_4; hence [g,f] in dom p by A4, RELAT_1:61; ::_thesis: verum end; A10: CatStr(# O,M,d,c,p #) is Category-like proof thus for f, g being Morphism of CatStr(# O,M,d,c,p #) holds ( [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) iff dom g = cod f ) by A8; :: according to CAT_1:def_6 ::_thesis: verum end; A11: CatStr(# O,M,d,c,p #) is transitive proof thus for f, g being Morphism of CatStr(# O,M,d,c,p #) st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def_7 ::_thesis: verum proof let f, g be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) reconsider ff = f, gg = g as Morphism of C by A5; A12: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49; assume A13: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) A14: [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) by A13, A8; A15: p . (g,f) = g (*) f by A13, A8, CAT_1:def_1; A16: dom p c= dom the Comp of C by A4, RELAT_1:60; A17: p . [g,f] = the Comp of C . (g,f) by A4, A8, A13, FUNCT_1:47 .= gg (*) ff by A16, A14, CAT_1:def_1 ; thus dom (g (*) f) = dom (gg (*) ff) by A17, A2, A15, FUNCT_1:49 .= dom ff by A13, A12, CAT_1:def_7 .= dom f by A2, FUNCT_1:49 ; ::_thesis: cod (g (*) f) = cod g thus cod (g (*) f) = cod (gg (*) ff) by A17, A3, A15, FUNCT_1:49 .= cod gg by A13, A12, CAT_1:def_7 .= cod g by A3, FUNCT_1:49 ; ::_thesis: verum end; end; A18: CatStr(# O,M,d,c,p #) is associative proof thus for f, g, h being Morphism of CatStr(# O,M,d,c,p #) st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def_8 ::_thesis: verum proof let f, g, h be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f ) reconsider ff = f, gg = g, hh = h as Morphism of C by A5; assume that A19: dom h = cod g and A20: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f A21: h (*) g = the Comp of CatStr(# O,M,d,c,p #) . (h,g) by A19, A8, CAT_1:def_1; A22: g (*) f = the Comp of CatStr(# O,M,d,c,p #) . (g,f) by A20, A8, CAT_1:def_1; A23: dom (h (*) g) = dom g by A11, A19, CAT_1:def_7; A24: ( c . g = cod gg & d . g = dom gg ) by A2, A3, FUNCT_1:49; A25: c . f = cod ff by A3, FUNCT_1:49; A26: ( f is Morphism of C & d . h = dom hh ) by A2, A5, FUNCT_1:49; A27: dom gg = d . g by A2, FUNCT_1:49 .= cod ff by A3, A20, FUNCT_1:49 ; then A28: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:16; A29: dom hh = d . h by A2, FUNCT_1:49 .= cod gg by A3, A19, FUNCT_1:49 ; then A30: cod (gg (*) ff) = dom hh by A27, CAT_1:def_7; A31: hh (*) gg = the Comp of C . (hh,gg) by A29, CAT_1:16; A32: cod ff = dom (hh (*) gg) by A27, A29, CAT_1:def_7; A33: cod (g (*) f) = cod g by A11, A20, CAT_1:def_7; hence h (*) (g (*) f) = the Comp of CatStr(# O,M,d,c,p #) . (h,( the Comp of CatStr(# O,M,d,c,p #) . (g,f))) by A22, A19, A8, CAT_1:def_1 .= the Comp of C . [h,(p . [g,f])] by A4, A8, A19, A33, A22, FUNCT_1:47 .= the Comp of C . (hh,(gg (*) ff)) by A4, A8, A20, A28, FUNCT_1:47 .= hh (*) (gg (*) ff) by A30, CAT_1:16 .= (hh (*) gg) (*) ff by A19, A20, A26, A24, A25, CAT_1:def_8 .= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A31, A32, CAT_1:16 .= the Comp of C . [(p . [h,g]),f] by A4, A8, A19, FUNCT_1:47 .= the Comp of CatStr(# O,M,d,c,p #) . (( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),f) by A4, A8, A20, A23, A21, FUNCT_1:47 .= (h (*) g) (*) f by A21, A20, A8, A23, CAT_1:def_1 ; ::_thesis: verum end; end; A34: CatStr(# O,M,d,c,p #) is reflexive proof let b be Object of CatStr(# O,M,d,c,p #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} b in O ; then reconsider bb = b as Object of C ; A35: Hom (bb,bb) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; id bb in Hom (bb,bb) by CAT_1:27; then reconsider ii = id bb as Morphism of CatStr(# O,M,d,c,p #) by A35, TARSKI:def_4, A1; A36: dom ii = dom (id bb) by A2, FUNCT_1:49 .= bb ; cod ii = cod (id bb) by A3, FUNCT_1:49 .= bb ; then ii in Hom (b,b) by A36; hence Hom (b,b) <> {} ; ::_thesis: verum end; CatStr(# O,M,d,c,p #) is with_identities proof let a be Element of CatStr(# O,M,d,c,p #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of CatStr(# O,M,d,c,p #) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) a in O ; then reconsider aa = a as Object of C ; A37: Hom (aa,aa) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; id aa in Hom (aa,aa) by CAT_1:27; then reconsider ii = id aa as Morphism of CatStr(# O,M,d,c,p #) by A37, TARSKI:def_4, A1; A38: dom ii = dom (id aa) by A2, FUNCT_1:49 .= aa ; A39: cod ii = cod (id aa) by A3, FUNCT_1:49 .= aa ; then reconsider ii = ii as Morphism of a,a by A38, CAT_1:4; take ii ; ::_thesis: for b1 being Element of the carrier of CatStr(# O,M,d,c,p #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) let b be Element of CatStr(# O,M,d,c,p #); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) ) b in O ; then reconsider bb = b as Object of C ; thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) proof assume A40: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g let g be Morphism of a,b; ::_thesis: g (*) ii = g reconsider gg = g as Morphism of C by A5; A41: dom gg = dom g by A2, FUNCT_1:49 .= aa by A40, CAT_1:5 ; A42: cod (id aa) = aa ; cod gg = cod g by A3, FUNCT_1:49 .= bb by A40, CAT_1:5 ; then reconsider gg = gg as Morphism of aa,bb by A41, CAT_1:4; A43: dom g = a by A40, CAT_1:5; hence g (*) ii = p . (g,ii) by CAT_1:def_1, A39, A8 .= the Comp of C . (gg,(id aa)) by FUNCT_1:47, A43, A4, A39, A8 .= gg (*) (id aa) by A41, CAT_1:16, A42 .= g by A41, CAT_1:22 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ::_thesis: verum proof assume A44: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f let g be Morphism of b,a; ::_thesis: ii (*) g = g reconsider gg = g as Morphism of C by A5; A45: cod gg = cod g by A3, FUNCT_1:49 .= aa by A44, CAT_1:5 ; A46: dom (id aa) = aa ; dom gg = dom g by A2, FUNCT_1:49 .= bb by A44, CAT_1:5 ; then reconsider gg = gg as Morphism of bb,aa by A45, CAT_1:4; A47: cod g = a by A44, CAT_1:5; hence ii (*) g = p . (ii,g) by CAT_1:def_1, A38, A8 .= the Comp of C . ((id aa),gg) by FUNCT_1:47, A4, A47, A38, A8 .= (id aa) (*) gg by A45, CAT_1:16, A46 .= g by A45, CAT_1:21 ; ::_thesis: verum end; end; hence CatStr(# O,M,d,c,p #) is Category by A10, A11, A18, A34; ::_thesis: verum end; Lm2: for C being Category for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Subcategory of C proof let C be Category; ::_thesis: for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Subcategory of C let O be non empty Subset of the carrier of C; ::_thesis: for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Subcategory of C let M be non empty set ; ::_thesis: for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Subcategory of C let d, c be Function of M,O; ::_thesis: for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Subcategory of C let p be PartFunc of [:M,M:],M; ::_thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is Subcategory of C let i be Function of O,M; ::_thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Subcategory of C ) set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; assume that A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and A2: d = the Source of C | M and A3: c = the Target of C | M and A4: p = the Comp of C || M ; ::_thesis: CatStr(# O,M,d,c,p #) is Subcategory of C set B = CatStr(# O,M,d,c,p #); A5: now__::_thesis:_for_f_being_Morphism_of_CatStr(#_O,M,d,c,p_#)_holds_f_is_Morphism_of_C let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: f is Morphism of C consider X being set such that A6: f in X and A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def_4; ex a, b being Object of C st ( X = Hom (a,b) & a in O & b in O ) by A7; hence f is Morphism of C by A6; ::_thesis: verum end; A8: for a, b being Object of CatStr(# O,M,d,c,p #) for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) proof let a, b be Object of CatStr(# O,M,d,c,p #); ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) ) assume A9: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Hom_(a,b)_implies_x_in_Hom_(a9,b9)_)_&_(_x_in_Hom_(a9,b9)_implies_x_in_Hom_(a,b)_)_) let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) ) thus ( x in Hom (a,b) implies x in Hom (a9,b9) ) ::_thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) ) proof assume A10: x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ; reconsider f9 = f as Morphism of C by A5; cod f = cod f9 by A3, FUNCT_1:49; then A11: b = cod f9 by A10, CAT_1:1; dom f = dom f9 by A2, FUNCT_1:49; then a = dom f9 by A10, CAT_1:1; hence x in Hom (a9,b9) by A9, A11; ::_thesis: verum end; assume A12: x in Hom (a9,b9) ; ::_thesis: x in Hom (a,b) then reconsider f9 = x as Morphism of C ; Hom (a9,b9) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A9; then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def_4; cod f = cod f9 by A3, FUNCT_1:49; then A13: cod f = b9 by A12, CAT_1:1; dom f = dom f9 by A2, FUNCT_1:49; then dom f = a9 by A12, CAT_1:1; hence x in Hom (a,b) by A9, A13; ::_thesis: verum end; hence Hom (a,b) = Hom (a9,b9) by TARSKI:1; ::_thesis: verum end; reconsider B = CatStr(# O,M,d,c,p #) as Category by Lm1, A1, A2, A3, A4; A14: for a being Object of B for a9 being Object of C st a = a9 holds id a = id a9 proof let a be Object of B; ::_thesis: for a9 being Object of C st a = a9 holds id a = id a9 let a9 be Object of C; ::_thesis: ( a = a9 implies id a = id a9 ) assume A15: a = a9 ; ::_thesis: id a = id a9 A16: Hom (a9,a9) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A15; A17: id a9 in Hom (a9,a9) by CAT_1:27; then reconsider ii = id a9 as Morphism of B by A16, A1, TARSKI:def_4; A18: dom ii = dom (id a9) by A2, FUNCT_1:49 .= a9 ; A19: cod ii = cod (id a9) by A3, FUNCT_1:49 .= a9 ; ii in Hom (a,a) by A17, A8, A15; then reconsider ii = ii as Morphism of a,a by CAT_1:def_5; A20: for f, g being Morphism of B holds ( [g,f] in dom p iff d . g = c . f ) proof let f, g be Morphism of B; ::_thesis: ( [g,f] in dom p iff d . g = c . f ) reconsider gg = g, ff = f as Morphism of C by A5; A21: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49; thus ( [g,f] in dom p implies d . g = c . f ) ::_thesis: ( d . g = c . f implies [g,f] in dom p ) proof assume [g,f] in dom p ; ::_thesis: d . g = c . f then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61; then [gg,ff] in dom the Comp of C by XBOOLE_0:def_4; hence d . g = c . f by A21, CAT_1:def_6; ::_thesis: verum end; assume d . g = c . f ; ::_thesis: [g,f] in dom p then [g,f] in dom the Comp of C by A21, CAT_1:def_6; then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def_4; hence [g,f] in dom p by A4, RELAT_1:61; ::_thesis: verum end; for b being Object of B holds ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) proof let b be Object of B; ::_thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) b in O ; then reconsider bb = b as Element of C ; thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) proof assume A22: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds f (*) ii = f let g be Morphism of a,b; ::_thesis: g (*) ii = g reconsider gg = g as Morphism of C by A5; A23: dom gg = dom g by A2, FUNCT_1:49 .= a9 by A15, CAT_1:5, A22 ; A24: cod (id a9) = a9 ; cod gg = cod g by A3, FUNCT_1:49 .= bb by A22, CAT_1:5 ; then reconsider gg = gg as Morphism of a9,bb by A23, CAT_1:4; A25: dom g = a by A22, CAT_1:5; hence g (*) ii = p . (g,ii) by CAT_1:def_1, A19, A20, A15 .= the Comp of C . (gg,(id a9)) by FUNCT_1:47, A19, A20, A15, A4, A25 .= gg (*) (id a9) by A23, CAT_1:16, A24 .= g by A23, CAT_1:22 ; ::_thesis: verum end; assume A26: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f let g be Morphism of b,a; ::_thesis: ii (*) g = g reconsider gg = g as Morphism of C by A5; A27: cod gg = cod g by A3, FUNCT_1:49 .= a9 by A15, CAT_1:5, A26 ; A28: dom (id a9) = a9 ; dom gg = dom g by A2, FUNCT_1:49 .= bb by A26, CAT_1:5 ; then reconsider gg = gg as Morphism of bb,a9 by A27, CAT_1:4; A29: cod g = a by A26, CAT_1:5; hence ii (*) g = p . (ii,g) by CAT_1:def_1, A18, A20, A15 .= the Comp of C . ((id a9),gg) by FUNCT_1:47, A18, A20, A15, A4, A29 .= (id a9) (*) gg by A27, CAT_1:16, A28 .= g by A27, CAT_1:21 ; ::_thesis: verum end; hence id a = id a9 by CAT_1:def_12; ::_thesis: verum end; ( ( for a, b being Object of B for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) ) & the Comp of B c= the Comp of C ) by A4, A8, RELAT_1:59; hence CatStr(# O,M,d,c,p #) is Subcategory of C by A14, Def4; ::_thesis: verum end; theorem :: CAT_2:21 for C being Category for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is full Subcategory of C proof let C be Category; ::_thesis: for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is full Subcategory of C let O be non empty Subset of the carrier of C; ::_thesis: for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is full Subcategory of C let M be non empty set ; ::_thesis: for d, c being Function of M,O for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is full Subcategory of C let d, c be Function of M,O; ::_thesis: for p being PartFunc of [:M,M:],M for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is full Subcategory of C let p be PartFunc of [:M,M:],M; ::_thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds CatStr(# O,M,d,c,p #) is full Subcategory of C let i be Function of O,M; ::_thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is full Subcategory of C ) set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; assume that A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and A2: d = the Source of C | M and A3: c = the Target of C | M and A4: p = the Comp of C || M ; ::_thesis: CatStr(# O,M,d,c,p #) is full Subcategory of C set B = CatStr(# O,M,d,c,p #); A5: now__::_thesis:_for_f_being_Morphism_of_CatStr(#_O,M,d,c,p_#)_holds_f_is_Morphism_of_C let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: f is Morphism of C consider X being set such that A6: f in X and A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def_4; ex a, b being Object of C st ( X = Hom (a,b) & a in O & b in O ) by A7; hence f is Morphism of C by A6; ::_thesis: verum end; A8: for a, b being Object of CatStr(# O,M,d,c,p #) for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) proof let a, b be Object of CatStr(# O,M,d,c,p #); ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) = Hom (a9,b9) let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) ) assume A9: ( a = a9 & b = b9 ) ; ::_thesis: Hom (a,b) = Hom (a9,b9) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Hom_(a,b)_implies_x_in_Hom_(a9,b9)_)_&_(_x_in_Hom_(a9,b9)_implies_x_in_Hom_(a,b)_)_) let x be set ; ::_thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) ) thus ( x in Hom (a,b) implies x in Hom (a9,b9) ) ::_thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) ) proof assume A10: x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ; reconsider f9 = f as Morphism of C by A5; cod f = cod f9 by A3, FUNCT_1:49; then A11: b = cod f9 by A10, CAT_1:1; dom f = dom f9 by A2, FUNCT_1:49; then a = dom f9 by A10, CAT_1:1; hence x in Hom (a9,b9) by A9, A11; ::_thesis: verum end; assume A12: x in Hom (a9,b9) ; ::_thesis: x in Hom (a,b) then reconsider f9 = x as Morphism of C ; Hom (a9,b9) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A9; then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def_4; cod f = cod f9 by A3, FUNCT_1:49; then A13: cod f = b9 by A12, CAT_1:1; dom f = dom f9 by A2, FUNCT_1:49; then dom f = a9 by A12, CAT_1:1; hence x in Hom (a,b) by A9, A13; ::_thesis: verum end; hence Hom (a,b) = Hom (a9,b9) by TARSKI:1; ::_thesis: verum end; reconsider B = CatStr(# O,M,d,c,p #) as Subcategory of C by Lm2, A1, A2, A3, A4; B is full by A8, Def6; hence CatStr(# O,M,d,c,p #) is full Subcategory of C ; ::_thesis: verum end; theorem :: CAT_2:22 for C being Category for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) proof let C be Category; ::_thesis: for O being non empty Subset of the carrier of C for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) let O be non empty Subset of the carrier of C; ::_thesis: for M being non empty set for d, c being Function of M,O for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) let M be non empty set ; ::_thesis: for d, c being Function of M,O for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) let d, c be Function of M,O; ::_thesis: for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) let p be PartFunc of [:M,M:],M; ::_thesis: ( CatStr(# O,M,d,c,p #) is full Subcategory of C implies ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) ) set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; set B = CatStr(# O,M,d,c,p #); assume A1: CatStr(# O,M,d,c,p #) is full Subcategory of C ; ::_thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) A2: for f being Morphism of CatStr(# O,M,d,c,p #) holds ( d . f = the Source of C . f & c . f = the Target of C . f ) proof let f be Morphism of CatStr(# O,M,d,c,p #); ::_thesis: ( d . f = the Source of C . f & c . f = the Target of C . f ) reconsider f9 = f as Morphism of C by A1, Th8; ( dom f = dom f9 & cod f = cod f9 ) by A1, Th9; hence ( d . f = the Source of C . f & c . f = the Target of C . f ) ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_M_implies_x_in_union__{__(Hom_(a,b))_where_a,_b_is_Object_of_C_:_(_a_in_O_&_b_in_O_)__}__)_&_(_x_in_union__{__(Hom_(a,b))_where_a,_b_is_Object_of_C_:_(_a_in_O_&_b_in_O_)__}__implies_x_in_M_)_) let x be set ; ::_thesis: ( ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) & ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M ) ) thus ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) ::_thesis: ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M ) proof assume x in M ; ::_thesis: x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ; reconsider f9 = f as Morphism of C by A1, Th8; set a9 = dom f9; set b9 = cod f9; ( the Source of CatStr(# O,M,d,c,p #) . f = the Source of C . f9 & the Target of CatStr(# O,M,d,c,p #) . f = the Target of C . f9 ) by A2; then ( f in Hom ((dom f9),(cod f9)) & Hom ((dom f9),(cod f9)) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) ; hence x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def_4; ::_thesis: verum end; assume x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; ::_thesis: x in M then consider X being set such that A3: x in X and A4: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def_4; consider a9, b9 being Object of C such that A5: X = Hom (a9,b9) and A6: ( a9 in O & b9 in O ) by A4; reconsider a = a9, b = b9 as Object of CatStr(# O,M,d,c,p #) by A6; Hom (a,b) = Hom (a9,b9) by A1, Def6; hence x in M by A3, A5; ::_thesis: verum end; hence M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:1; ::_thesis: ( d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) then reconsider d9 = the Source of C | M, c9 = the Target of C | M as Function of M,O by Th20; set p9 = the Comp of C || M; now__::_thesis:_for_f_being_Element_of_M_holds_d_._f_=_d9_._f let f be Element of M; ::_thesis: d . f = d9 . f d . f = the Source of C . f by A2; hence d . f = d9 . f by FUNCT_1:49; ::_thesis: verum end; hence d = the Source of C | M by FUNCT_2:63; ::_thesis: ( c = the Target of C | M & p = the Comp of C || M ) now__::_thesis:_for_f_being_Element_of_M_holds_c_._f_=_c9_._f let f be Element of M; ::_thesis: c . f = c9 . f c . f = the Target of C . f by A2; hence c . f = c9 . f by FUNCT_1:49; ::_thesis: verum end; hence c = the Target of C | M by FUNCT_2:63; ::_thesis: p = the Comp of C || M now__::_thesis:_(_dom_p_=_dom_(_the_Comp_of_C_||_M)_&_(_for_x_being_set_st_x_in_dom_p_holds_ p_._x_=_(_the_Comp_of_C_||_M)_._x_)_) A7: dom p c= [:M,M:] by RELAT_1:def_18; A8: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61; the Comp of CatStr(# O,M,d,c,p #) c= the Comp of C by A1, Def4; then dom p c= dom the Comp of C by GRFUNC_1:2; then A9: dom p c= dom ( the Comp of C || M) by A7, A8, XBOOLE_1:19; dom ( the Comp of C || M) c= dom p proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ( the Comp of C || M) or x in dom p ) assume A10: x in dom ( the Comp of C || M) ; ::_thesis: x in dom p then x in [:M,M:] by A8, XBOOLE_0:def_4; then consider g, f being Element of M such that A11: x = [g,f] by DOMAIN_1:1; reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ; reconsider f9 = f, g9 = g as Morphism of C by A1, Th8; [g,f] in dom the Comp of C by A8, A10, A11, XBOOLE_0:def_4; then A12: dom g9 = cod f9 by CAT_1:15; ( cod f = cod f9 & dom g = dom g9 ) by A1, Th9; hence x in dom p by A1, A11, A12, CAT_1:15; ::_thesis: verum end; hence dom p = dom ( the Comp of C || M) by A9, XBOOLE_0:def_10; ::_thesis: for x being set st x in dom p holds p . x = ( the Comp of C || M) . x let x be set ; ::_thesis: ( x in dom p implies p . x = ( the Comp of C || M) . x ) assume A13: x in dom p ; ::_thesis: p . x = ( the Comp of C || M) . x then consider g, f being Element of M such that A14: x = [g,f] by A7, DOMAIN_1:1; reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ; A15: dom g = cod f by A1, A13, A14, CAT_1:15; reconsider f9 = f, g9 = g as Morphism of C by A1, Th8; A16: ( cod f = cod f9 & dom g = dom g9 ) by A1, Th9; p . x = p . (g,f) by A14; hence p . x = g (*) f by A1, A15, CAT_1:16 .= g9 (*) f9 by A1, A15, Th11 .= the Comp of C . (g9,f9) by A16, A1, A13, A14, CAT_1:15, CAT_1:16 .= ( the Comp of C || M) . x by A9, A13, A14, FUNCT_1:47 ; ::_thesis: verum end; hence p = the Comp of C || M by FUNCT_1:2; ::_thesis: verum end; definition let X1, X2, Y1, Y2 be non empty set ; let f1 be Function of X1,Y1; let f2 be Function of X2,Y2; :: original: [: redefine func[:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:]; coherence [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] proof [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] ; hence [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] ; ::_thesis: verum end; end; definition let A, B be non empty set ; let f be PartFunc of [:A,A:],A; let g be PartFunc of [:B,B:],B; :: original: |: redefine func|:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:]; coherence |:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:] by FUNCT_4:59; end; definition let C, D be Category; func[:C,D:] -> Category equals :: CAT_2:def 7 CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); coherence CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category proof set O = [: the carrier of C, the carrier of D:]; set M = [: the carrier' of C, the carrier' of D:]; set d = [: the Source of C, the Source of D:]; set c = [: the Target of C, the Target of D:]; set p = |: the Comp of C, the Comp of D:|; A1: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) proof let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) ) A2: ( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [( the Source of C . (g `1)),( the Source of D . (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [( the Target of C . (f `1)),( the Target of D . (f `2))] ) by FUNCT_3:75; assume A3: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; ::_thesis: ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21; then ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by A2, A3, XTUPLE_0:1; hence ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by CAT_1:def_6; ::_thesis: verum end; A4: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [g,f] in dom |: the Comp of C, the Comp of D:| holds ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) proof let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [g,f] in dom |: the Comp of C, the Comp of D:| implies ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) ) assume A5: [g,f] in dom |: the Comp of C, the Comp of D:| ; ::_thesis: ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21; then ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A5, FUNCT_4:54; hence ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by CAT_1:def_6; ::_thesis: verum end; set B = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); A6: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category-like proof let ff, gg be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_6 ::_thesis: ( ( not [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ) ) reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ; A7: ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21; thus ( [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) implies dom gg = cod ff ) ::_thesis: ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ) proof A8: ( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [(dom (g `1)),(dom (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [(cod (f `1)),(cod (f `2))] ) by FUNCT_3:75; assume A9: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; ::_thesis: dom gg = cod ff then dom (g `1) = cod (f `1) by A4; hence dom gg = cod ff by A4, A7, A9, A8; ::_thesis: verum end; assume dom gg = cod ff ; ::_thesis: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) then ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A1; hence [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A7, FUNCT_4:54; ::_thesis: verum end; A10: for f, g being Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds ( [g,f] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) iff dom g = cod f ) by A6, CAT_1:def_6; A11: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] proof let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] ) reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; assume [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; ::_thesis: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] then A12: dom gg = cod ff ; ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21; hence |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A12, A10, FUNCT_4:55; ::_thesis: verum end; A13: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g ) proof let f, g be Element of [: the carrier' of C, the carrier' of D:]; ::_thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g ) ) reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; A14: ( f = [(f `1),(f `2)] & [: the Source of C, the Source of D:] . ((f `1),(f `2)) = [(dom (f `1)),(dom (f `2))] ) by FUNCT_3:75, MCART_1:21; assume A15: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; ::_thesis: ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g ) then A16: the Comp of C . [(g `1),(f `1)] in the carrier' of C by A1, PARTFUN1:4; then A17: the Comp of C . ((g `1),(f `1)) in dom the Source of C by FUNCT_2:def_1; dom gg = cod ff by A15; then A18: [gg,ff] in dom |: the Comp of C, the Comp of D:| by A6, CAT_1:def_6; then A19: dom (g `1) = cod (f `1) by A4; then [(g `1),(f `1)] in dom the Comp of C by CAT_1:def_6; then A20: the Comp of C . ((g `1),(f `1)) = (g `1) (*) (f `1) by CAT_1:def_1; A21: dom ((g `1) (*) (f `1)) = dom (f `1) by A19, CAT_1:def_7; A22: the Comp of D . [(g `2),(f `2)] in the carrier' of D by A1, A15, PARTFUN1:4; then A23: the Comp of D . ((g `2),(f `2)) in dom the Source of D by FUNCT_2:def_1; A24: dom (g `2) = cod (f `2) by A4, A18; then [(g `2),(f `2)] in dom the Comp of D by CAT_1:def_6; then A25: the Comp of D . ((g `2),(f `2)) = (g `2) (*) (f `2) by CAT_1:def_1; A26: dom ((g `2) (*) (f `2)) = dom (f `2) by A24, CAT_1:def_7; thus [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15 .= [: the Source of C, the Source of D:] . f by A14, A21, A26, A17, A23, A20, A25, FUNCT_3:def_8 ; ::_thesis: [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g A27: ( g = [(g `1),(g `2)] & [: the Target of C, the Target of D:] . ((g `1),(g `2)) = [( the Target of C . (g `1)),( the Target of D . (g `2))] ) by FUNCT_3:75, MCART_1:21; A28: cod ((g `2) (*) (f `2)) = cod (g `2) by A24, CAT_1:def_7; A29: cod ((g `1) (*) (f `1)) = cod (g `1) by A19, CAT_1:def_7; A30: the Comp of D . ((g `2),(f `2)) in dom the Target of D by A22, FUNCT_2:def_1; A31: the Comp of C . ((g `1),(f `1)) in dom the Target of C by A16, FUNCT_2:def_1; thus [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15 .= [: the Target of C, the Target of D:] . g by A27, A29, A28, A31, A30, A20, A25, FUNCT_3:def_8 ; ::_thesis: verum end; A32: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is transitive proof let ff, gg be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) ) reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ; assume A33: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) then A34: the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) . (gg,ff) = gg (*) ff by A10, CAT_1:def_1; thus dom (gg (*) ff) = dom ff by A13, A33, A34; ::_thesis: cod (gg (*) ff) = cod gg thus cod (gg (*) ff) = cod gg by A13, A33, A34; ::_thesis: verum end; A35: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is associative proof let ff, gg, hh be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff ) reconsider f = ff, g = gg, h = hh as Element of [: the carrier' of C, the carrier' of D:] ; assume that A36: dom hh = cod gg and A37: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff A38: ( the Comp of C . [(h `1),(g `1)] in the carrier' of C & the Comp of D . [(h `2),(g `2)] in the carrier' of D ) by A1, A36, PARTFUN1:4; ( the Comp of C . [(g `1),(f `1)] in the carrier' of C & the Comp of D . [(g `2),(f `2)] in the carrier' of D ) by A1, A37, PARTFUN1:4; then reconsider pgf = [( the Comp of C . [(g `1),(f `1)]),( the Comp of D . [(g `2),(f `2)])], phg = [( the Comp of C . [(h `1),(g `1)]),( the Comp of D . [(h `2),(g `2)])] as Element of [: the carrier' of C, the carrier' of D:] by A38, ZFMISC_1:87; set pgf2 = pgf `2 ; set phg2 = phg `2 ; set pgf1 = pgf `1 ; set phg1 = phg `1 ; A39: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A11, A37; A40: [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) by A13, A36, A37; A41: |: the Comp of C, the Comp of D:| . (h,g) = [( the Comp of C . ((h `1),(g `1))),( the Comp of D . ((h `2),(g `2)))] by A11, A36; [(h `2),(g `2)] in dom the Comp of D by A1, A36; then A42: dom (h `2) = cod (g `2) by CAT_1:def_6; [(h `1),(g `1)] in dom the Comp of C by A1, A36; then A43: dom (h `1) = cod (g `1) by CAT_1:def_6; [(g `2),(f `2)] in dom the Comp of D by A1, A37; then A44: dom (g `2) = cod (f `2) by CAT_1:def_6; [(g `1),(f `1)] in dom the Comp of C by A1, A37; then A45: dom (g `1) = cod (f `1) by CAT_1:def_6; A46: [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (h,g)) = [: the Target of C, the Target of D:] . f by A13, A36, A37; A47: ( pgf `1 = the Comp of C . ((g `1),(f `1)) & phg `1 = the Comp of C . ((h `1),(g `1)) ) by MCART_1:7; A48: ( pgf `2 = the Comp of D . ((g `2),(f `2)) & phg `2 = the Comp of D . ((h `2),(g `2)) ) by MCART_1:7; A49: (h `2) (*) ((g `2) (*) (f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A42, A44, CAT_1:def_8; A50: gg (*) ff = |: the Comp of C, the Comp of D:| . (g,f) by A37, A10, CAT_1:def_1; then A51: cod (gg (*) ff) = dom hh by A13, A36, A37; A52: hh (*) gg = |: the Comp of C, the Comp of D:| . (h,g) by A36, A10, CAT_1:def_1; then A53: dom (hh (*) gg) = cod ff by A13, A36, A37; A54: cod ((g `1) (*) (f `1)) = cod (g `1) by A45, CAT_1:def_7; A55: pgf `1 = (g `1) (*) (f `1) by A47, A45, CAT_1:16; A56: cod ((g `2) (*) (f `2)) = cod (g `2) by A44, CAT_1:def_7; pgf `2 = (g `2) (*) (f `2) by A48, A44, CAT_1:16; then A57: the Comp of D . ((h `2),(pgf `2)) = (h `2) (*) ((g `2) (*) (f `2)) by A42, A56, CAT_1:16; A58: dom ((h `1) (*) (g `1)) = dom (g `1) by A43, CAT_1:def_7; A59: phg `1 = (h `1) (*) (g `1) by A47, A43, CAT_1:16; A60: dom ((h `2) (*) (g `2)) = dom (g `2) by A42, CAT_1:def_7; phg `2 = (h `2) (*) (g `2) by A48, A42, CAT_1:16; then A61: the Comp of D . ((phg `2),(f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A44, A60, CAT_1:16; thus hh (*) (gg (*) ff) = |: the Comp of C, the Comp of D:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) by A51, A50, A10, CAT_1:def_1 .= [( the Comp of C . ((h `1),(pgf `1))),( the Comp of D . ((h `2),(pgf `2)))] by A40, A11, A39 .= [((h `1) (*) ((g `1) (*) (f `1))),((h `2) (*) ((g `2) (*) (f `2)))] by A55, A57, A43, A54, CAT_1:16 .= [(((h `1) (*) (g `1)) (*) (f `1)),(((h `2) (*) (g `2)) (*) (f `2))] by A43, A45, A49, CAT_1:def_8 .= [( the Comp of C . ((phg `1),(f `1))),( the Comp of D . ((phg `2),(f `2)))] by A59, A61, A45, A58, CAT_1:16 .= |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) by A46, A11, A41 .= (hh (*) gg) (*) ff by A53, A10, A52, CAT_1:def_1 ; ::_thesis: verum end; A62: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is reflexive proof let b be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} reconsider bb = b as Element of [: the carrier of C, the carrier of D:] ; reconsider ii = [(id (bb `1)),(id (bb `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; A63: cod ii = [: the Target of C, the Target of D:] . ((id (bb `1)),(id (bb `2))) .= [(cod (id (bb `1))),(cod (id (bb `2)))] by FUNCT_3:75 .= [(bb `1),(cod (id (bb `2)))] .= [(bb `1),(bb `2)] .= bb by MCART_1:21 ; dom ii = [: the Source of C, the Source of D:] . ((id (bb `1)),(id (bb `2))) .= [(dom (id (bb `1))),(dom (id (bb `2)))] by FUNCT_3:75 .= [(bb `1),(dom (id (bb `2)))] .= [(bb `1),(bb `2)] .= bb by MCART_1:21 ; then [(id (bb `1)),(id (bb `2))] in Hom (b,b) by A63; hence Hom (b,b) <> {} ; ::_thesis: verum end; CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is with_identities proof let a be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of [: the carrier of C, the carrier of D:] ; reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; A64: cod ii = [: the Target of C, the Target of D:] . ((id (aa `1)),(id (aa `2))) .= [(cod (id (aa `1))),(cod (id (aa `2)))] by FUNCT_3:75 .= [(aa `1),(cod (id (aa `2)))] .= [(aa `1),(aa `2)] .= aa by MCART_1:21 ; A65: dom ii = [: the Source of C, the Source of D:] . ((id (aa `1)),(id (aa `2))) .= [(dom (id (aa `1))),(dom (id (aa `2)))] by FUNCT_3:75 .= [(aa `1),(dom (id (aa `2)))] .= [(aa `1),(aa `2)] .= aa by MCART_1:21 ; then reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of a,a by A64, CAT_1:4; take ii ; ::_thesis: for b1 being Element of the carrier of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) let b be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) proof assume A66: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g let g be Morphism of a,b; ::_thesis: g (*) ii = g reconsider gg = g as Element of [: the carrier' of C, the carrier' of D:] ; cod ii = dom g by A66, CAT_1:5, A64; then A67: [g,ii] in dom |: the Comp of C, the Comp of D:| by A6, CAT_1:def_6; then A68: dom (gg `1) = cod ([(id (aa `1)),(id (aa `2))] `1) by A4 .= cod (id (aa `1)) ; A69: the Comp of C . ((gg `1),(id (aa `1))) = (gg `1) (*) (id (aa `1)) by CAT_1:16, A68 .= gg `1 by A68, CAT_1:22 ; A70: dom (gg `2) = cod ([(id (aa `1)),(id (aa `2))] `2) by A4, A67 .= cod (id (aa `2)) ; A71: the Comp of D . ((gg `2),(id (aa `2))) = (gg `2) (*) (id (aa `2)) by CAT_1:16, A70 .= gg `2 by A70, CAT_1:22 ; A72: cod ii = dom g by A64, A66, CAT_1:5; then [g,ii] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6, CAT_1:def_6; hence g (*) ii = |: the Comp of C, the Comp of D:| . (g,ii) by CAT_1:def_1 .= [( the Comp of C . ((gg `1),([(id (aa `1)),(id (aa `2))] `1))),( the Comp of D . ((gg `2),([(id (aa `1)),(id (aa `2))] `2)))] by A11, A72 .= g by A69, A71, MCART_1:21 ; ::_thesis: verum end; assume A73: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1 let g be Morphism of b,a; ::_thesis: ii (*) g = g reconsider gg = g as Element of [: the carrier' of C, the carrier' of D:] ; dom ii = cod g by A73, CAT_1:5, A65; then A74: [ii,g] in dom |: the Comp of C, the Comp of D:| by A6, CAT_1:def_6; then A75: cod (gg `1) = dom ([(id (aa `1)),(id (aa `2))] `1) by A4 .= dom (id (aa `1)) ; A76: the Comp of C . ((id (aa `1)),(gg `1)) = (id (aa `1)) (*) (gg `1) by CAT_1:16, A75 .= gg `1 by A75, CAT_1:21 ; A77: cod (gg `2) = dom ([(id (aa `1)),(id (aa `2))] `2) by A4, A74 .= dom (id (aa `2)) ; A78: the Comp of D . ((id (aa `2)),(gg `2)) = (id (aa `2)) (*) (gg `2) by CAT_1:16, A77 .= gg `2 by A77, CAT_1:21 ; A79: dom ii = cod g by A65, A73, CAT_1:5; then [ii,g] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6, CAT_1:def_6; hence ii (*) g = |: the Comp of C, the Comp of D:| . (ii,g) by CAT_1:def_1 .= [( the Comp of C . (([(id (aa `1)),(id (aa `2))] `1),(gg `1))),( the Comp of D . (([(id (aa `1)),(id (aa `2))] `2),(gg `2)))] by A11, A79 .= g by A76, A78, MCART_1:21 ; ::_thesis: verum end; hence CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category by A6, A32, A35, A62; ::_thesis: verum end; end; :: deftheorem defines [: CAT_2:def_7_:_ for C, D being Category holds [:C,D:] = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); theorem :: CAT_2:23 for C, D being Category holds ( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] & the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] & the Source of [:C,D:] = [: the Source of C, the Source of D:] & the Target of [:C,D:] = [: the Target of C, the Target of D:] & the Comp of [:C,D:] = |: the Comp of C, the Comp of D:| ) ; definition let C, D be Category; let c be Object of C; let d be Object of D; :: original: [ redefine func[c,d] -> Object of [:C,D:]; coherence [c,d] is Object of [:C,D:] proof thus [c,d] is Object of [:C,D:] ; ::_thesis: verum end; end; theorem :: CAT_2:24 canceled; theorem :: CAT_2:25 for C, D being Category for cd being Object of [:C,D:] ex c being Object of C ex d being Object of D st cd = [c,d] by DOMAIN_1:1; definition let C, D be Category; let f be Morphism of C; let g be Morphism of D; :: original: [ redefine func[f,g] -> Morphism of [:C,D:]; coherence [f,g] is Morphism of [:C,D:] proof thus [f,g] is Morphism of [:C,D:] ; ::_thesis: verum end; end; theorem :: CAT_2:26 canceled; theorem :: CAT_2:27 for C, D being Category for fg being Morphism of [:C,D:] ex f being Morphism of C ex g being Morphism of D st fg = [f,g] by DOMAIN_1:1; theorem Th28: :: CAT_2:28 for C, D being Category for f being Morphism of C for g being Morphism of D holds ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] ) proof let C, D be Category; ::_thesis: for f being Morphism of C for g being Morphism of D holds ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] ) let f be Morphism of C; ::_thesis: for g being Morphism of D holds ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] ) let g be Morphism of D; ::_thesis: ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] ) thus dom [f,g] = [: the Source of C, the Source of D:] . (f,g) .= [(dom f),(dom g)] by FUNCT_3:75 ; ::_thesis: cod [f,g] = [(cod f),(cod g)] thus cod [f,g] = [: the Target of C, the Target of D:] . (f,g) .= [(cod f),(cod g)] by FUNCT_3:75 ; ::_thesis: verum end; theorem Th29: :: CAT_2:29 for C, D being Category for f, f9 being Morphism of C for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] proof let C, D be Category; ::_thesis: for f, f9 being Morphism of C for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] let f, f9 be Morphism of C; ::_thesis: for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] let g, g9 be Morphism of D; ::_thesis: ( dom f9 = cod f & dom g9 = cod g implies [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] ) assume that A1: dom f9 = cod f and A2: dom g9 = cod g ; ::_thesis: [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] A3: ( [f9,f] in dom the Comp of C & [g9,g] in dom the Comp of D ) by A1, A2, CAT_1:15; ( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th28; hence [f9,g9] (*) [f,g] = |: the Comp of C, the Comp of D:| . ([f9,g9],[f,g]) by A1, A2, CAT_1:16 .= [( the Comp of C . (f9,f)),( the Comp of D . (g9,g))] by A3, FUNCT_4:def_3 .= [(f9 (*) f),( the Comp of D . (g9,g))] by A1, CAT_1:16 .= [(f9 (*) f),(g9 (*) g)] by A2, CAT_1:16 ; ::_thesis: verum end; theorem Th30: :: CAT_2:30 for C, D being Category for f, f9 being Morphism of C for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] proof let C, D be Category; ::_thesis: for f, f9 being Morphism of C for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] let f, f9 be Morphism of C; ::_thesis: for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] let g, g9 be Morphism of D; ::_thesis: ( dom [f9,g9] = cod [f,g] implies [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] ) assume A1: dom [f9,g9] = cod [f,g] ; ::_thesis: [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] ( [(dom f9),(dom g9)] = dom [f9,g9] & cod [f,g] = [(cod f),(cod g)] ) by Th28; then ( dom f9 = cod f & dom g9 = cod g ) by A1, XTUPLE_0:1; hence [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] by Th29; ::_thesis: verum end; theorem Th31: :: CAT_2:31 for C, D being Category for c being Object of C for d being Object of D holds id [c,d] = [(id c),(id d)] proof let C, D be Category; ::_thesis: for c being Object of C for d being Object of D holds id [c,d] = [(id c),(id d)] let c be Object of C; ::_thesis: for d being Object of D holds id [c,d] = [(id c),(id d)] let d be Object of D; ::_thesis: id [c,d] = [(id c),(id d)] A1: dom [(id c),(id d)] = [(dom (id c)),(dom (id d))] by Th28 .= [c,(dom (id d))] .= [c,d] ; cod [(id c),(id d)] = [(cod (id c)),(cod (id d))] by Th28 .= [c,(cod (id d))] .= [c,d] ; then reconsider m = [(id c),(id d)] as Morphism of [c,d],[c,d] by A1, CAT_1:4; for b being Object of [:C,D:] holds ( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) ) proof let b be Object of [:C,D:]; ::_thesis: ( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) ) thus ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) ::_thesis: ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) proof assume A2: Hom ([c,d],b) <> {} ; ::_thesis: for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f let f be Morphism of [c,d],b; ::_thesis: f (*) [(id c),(id d)] = f consider fc being Morphism of C, fd being Morphism of D such that A3: f = [fc,fd] by DOMAIN_1:1; A4: [c,d] = dom f by A2, CAT_1:5 .= [(dom fc),(dom fd)] by A3, Th28 ; then A5: c = dom fc by XTUPLE_0:1; then A6: cod (id c) = dom fc ; A7: d = dom fd by A4, XTUPLE_0:1; then cod (id d) = dom fd ; hence f (*) [(id c),(id d)] = [(fc (*) (id c)),(fd (*) (id d))] by A3, A6, Th29 .= [fc,(fd (*) (id d))] by A5, CAT_1:22 .= f by A3, A7, CAT_1:22 ; ::_thesis: verum end; assume A8: Hom (b,[c,d]) <> {} ; ::_thesis: for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f let f be Morphism of b,[c,d]; ::_thesis: [(id c),(id d)] (*) f = f consider fc being Morphism of C, fd being Morphism of D such that A9: f = [fc,fd] by DOMAIN_1:1; A10: [c,d] = cod f by A8, CAT_1:5 .= [(cod fc),(cod fd)] by A9, Th28 ; then A11: c = cod fc by XTUPLE_0:1; then A12: dom (id c) = cod fc ; A13: d = cod fd by A10, XTUPLE_0:1; then dom (id d) = cod fd ; hence [(id c),(id d)] (*) f = [((id c) (*) fc),((id d) (*) fd)] by A9, A12, Th29 .= [fc,((id d) (*) fd)] by A11, CAT_1:21 .= f by A9, A13, CAT_1:21 ; ::_thesis: verum end; then m = id [c,d] by CAT_1:def_12; hence id [c,d] = [(id c),(id d)] ; ::_thesis: verum end; theorem :: CAT_2:32 for C, D being Category for c, c9 being Object of C for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] proof let C, D be Category; ::_thesis: for c, c9 being Object of C for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] let c, c9 be Object of C; ::_thesis: for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] let d, d9 be Object of D; ::_thesis: Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Hom_([c,d],[c9,d9])_implies_x_in_[:(Hom_(c,c9)),(Hom_(d,d9)):]_)_&_(_x_in_[:(Hom_(c,c9)),(Hom_(d,d9)):]_implies_x_in_Hom_([c,d],[c9,d9])_)_) let x be set ; ::_thesis: ( ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) & ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) ) ) thus ( x in Hom ([c,d],[c9,d9]) implies x in [:(Hom (c,c9)),(Hom (d,d9)):] ) ::_thesis: ( x in [:(Hom (c,c9)),(Hom (d,d9)):] implies x in Hom ([c,d],[c9,d9]) ) proof assume A1: x in Hom ([c,d],[c9,d9]) ; ::_thesis: x in [:(Hom (c,c9)),(Hom (d,d9)):] then reconsider fg = x as Morphism of [c,d],[c9,d9] by CAT_1:def_5; A2: dom fg = [c,d] by A1, CAT_1:1; A3: cod fg = [c9,d9] by A1, CAT_1:1; consider x1, x2 being set such that A4: x1 in the carrier' of C and A5: x2 in the carrier' of D and A6: fg = [x1,x2] by ZFMISC_1:def_2; reconsider g = x2 as Morphism of D by A5; reconsider f = x1 as Morphism of C by A4; A7: cod fg = [(cod f),(cod g)] by A6, Th28; then A8: cod f = c9 by A3, XTUPLE_0:1; A9: cod g = d9 by A3, A7, XTUPLE_0:1; A10: dom fg = [(dom f),(dom g)] by A6, Th28; then dom g = d by A2, XTUPLE_0:1; then A11: g in Hom (d,d9) by A9; dom f = c by A2, A10, XTUPLE_0:1; then f in Hom (c,c9) by A8; hence x in [:(Hom (c,c9)),(Hom (d,d9)):] by A6, A11, ZFMISC_1:87; ::_thesis: verum end; assume x in [:(Hom (c,c9)),(Hom (d,d9)):] ; ::_thesis: x in Hom ([c,d],[c9,d9]) then consider x1, x2 being set such that A12: x1 in Hom (c,c9) and A13: x2 in Hom (d,d9) and A14: x = [x1,x2] by ZFMISC_1:def_2; reconsider g = x2 as Morphism of d,d9 by A13, CAT_1:def_5; reconsider f = x1 as Morphism of c,c9 by A12, CAT_1:def_5; ( cod f = c9 & cod g = d9 ) by A12, A13, CAT_1:1; then A15: cod [f,g] = [c9,d9] by Th28; ( dom f = c & dom g = d ) by A12, A13, CAT_1:1; then dom [f,g] = [c,d] by Th28; hence x in Hom ([c,d],[c9,d9]) by A14, A15; ::_thesis: verum end; hence Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):] by TARSKI:1; ::_thesis: verum end; theorem :: CAT_2:33 for C, D being Category for c, c9 being Object of C for f being Morphism of c,c9 for d, d9 being Object of D for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9] proof let C, D be Category; ::_thesis: for c, c9 being Object of C for f being Morphism of c,c9 for d, d9 being Object of D for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9] let c, c9 be Object of C; ::_thesis: for f being Morphism of c,c9 for d, d9 being Object of D for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9] let f be Morphism of c,c9; ::_thesis: for d, d9 being Object of D for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9] let d, d9 be Object of D; ::_thesis: for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9] let g be Morphism of d,d9; ::_thesis: ( Hom (c,c9) <> {} & Hom (d,d9) <> {} implies [f,g] is Morphism of [c,d],[c9,d9] ) assume A1: ( Hom (c,c9) <> {} & Hom (d,d9) <> {} ) ; ::_thesis: [f,g] is Morphism of [c,d],[c9,d9] then ( cod f = c9 & cod g = d9 ) by CAT_1:5; then A2: cod [f,g] = [c9,d9] by Th28; ( dom f = c & dom g = d ) by A1, CAT_1:5; then dom [f,g] = [c,d] by Th28; hence [f,g] is Morphism of [c,d],[c9,d9] by A2, CAT_1:4; ::_thesis: verum end; definition let C, C9, D be Category; let S be Functor of [:C,C9:],D; let m be Morphism of C; let m9 be Morphism of C9; :: original: . redefine funcS . (m,m9) -> Morphism of D; coherence S . (m,m9) is Morphism of D proof S . (m,m9) = S . [m,m9] ; hence S . (m,m9) is Morphism of D ; ::_thesis: verum end; end; theorem Th34: :: CAT_2:34 for C, C9, D being Category for S being Functor of [:C,C9:],D for c being Object of C holds (curry S) . (id c) is Functor of C9,D proof let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D for c being Object of C holds (curry S) . (id c) is Functor of C9,D let S be Functor of [:C,C9:],D; ::_thesis: for c being Object of C holds (curry S) . (id c) is Functor of C9,D let c be Object of C; ::_thesis: (curry S) . (id c) is Functor of C9,D reconsider S9 = S as Function of [: the carrier' of C, the carrier' of C9:], the carrier' of D ; reconsider T = (curry S9) . (id c) as Function of the carrier' of C9, the carrier' of D ; now__::_thesis:_(_(_for_c9_being_Object_of_C9_ex_d_being_Object_of_D_st_T_._(id_c9)_=_id_d_)_&_(_for_f_being_Morphism_of_C9_holds_ (_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C9_st_dom_g_=_cod_f_holds_ T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_) thus for c9 being Object of C9 ex d being Object of D st T . (id c9) = id d ::_thesis: ( ( for f being Morphism of C9 holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C9 st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) ) proof let c9 be Object of C9; ::_thesis: ex d being Object of D st T . (id c9) = id d consider d being Object of D such that A1: S . (id [c,c9]) = id d by CAT_1:62; take d ; ::_thesis: T . (id c9) = id d thus T . (id c9) = S . ((id c),(id c9)) by FUNCT_5:69 .= id d by A1, Th31 ; ::_thesis: verum end; A2: ( dom (id c) = c & cod (id c) = c ) ; thus for f being Morphism of C9 holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of C9 st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) proof let f be Morphism of C9; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) thus T . (id (dom f)) = S . ((id c),(id (dom f))) by FUNCT_5:69 .= S . (id [c,(dom f)]) by Th31 .= S . (id [(dom (id c)),(dom f)]) .= S . (id (dom [(id c),f])) by Th28 .= id (dom (S . ((id c),f))) by CAT_1:63 .= id (dom (T . f)) by FUNCT_5:69 ; ::_thesis: T . (id (cod f)) = id (cod (T . f)) thus T . (id (cod f)) = S . ((id c),(id (cod f))) by FUNCT_5:69 .= S . (id [c,(cod f)]) by Th31 .= S . (id [(cod (id c)),(cod f)]) .= S . (id (cod [(id c),f])) by Th28 .= id (cod (S . ((id c),f))) by CAT_1:63 .= id (cod (T . f)) by FUNCT_5:69 ; ::_thesis: verum end; let f, g be Morphism of C9; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) ) assume A3: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f) Hom (c,c) <> {} ; then A4: (id c) * (id c) = (id c) (*) (id c) by CAT_1:def_13; A5: ( dom [(id c),g] = [(dom (id c)),(dom g)] & cod [(id c),f] = [(cod (id c)),(cod f)] ) by Th28; thus T . (g (*) f) = S . (((id c) * (id c)),(g (*) f)) by FUNCT_5:69 .= S . ([(id c),g] (*) [(id c),f]) by A3, A2, A4, Th29 .= (S . ((id c),g)) (*) (S . ((id c),f)) by A3, A5, CAT_1:64 .= (T . g) (*) (S . ((id c),f)) by FUNCT_5:69 .= (T . g) (*) (T . f) by FUNCT_5:69 ; ::_thesis: verum end; hence (curry S) . (id c) is Functor of C9,D by CAT_1:61; ::_thesis: verum end; theorem Th35: :: CAT_2:35 for C, C9, D being Category for S being Functor of [:C,C9:],D for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D proof let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D let S be Functor of [:C,C9:],D; ::_thesis: for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D let c9 be Object of C9; ::_thesis: (curry' S) . (id c9) is Functor of C,D reconsider S9 = S as Function of [: the carrier' of C, the carrier' of C9:], the carrier' of D ; reconsider T = (curry' S9) . (id c9) as Function of the carrier' of C, the carrier' of D ; now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_D_st_T_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_ (_T_._(id_(dom_f))_=_id_(dom_(T_._f))_&_T_._(id_(cod_f))_=_id_(cod_(T_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ T_._(g_(*)_f)_=_(T_._g)_(*)_(T_._f)_)_) thus for c being Object of C ex d being Object of D st T . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) ) ) proof let c be Object of C; ::_thesis: ex d being Object of D st T . (id c) = id d consider d being Object of D such that A1: S . (id [c,c9]) = id d by CAT_1:62; take d ; ::_thesis: T . (id c) = id d thus T . (id c) = S . ((id c),(id c9)) by FUNCT_5:70 .= id d by A1, Th31 ; ::_thesis: verum end; A2: ( dom (id c9) = c9 & cod (id c9) = c9 ) ; thus for f being Morphism of C holds ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds T . (g (*) f) = (T . g) (*) (T . f) proof let f be Morphism of C; ::_thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) thus T . (id (dom f)) = S . ((id (dom f)),(id c9)) by FUNCT_5:70 .= S . (id [(dom f),c9]) by Th31 .= S . (id [(dom f),(dom (id c9))]) .= S . (id (dom [f,(id c9)])) by Th28 .= id (dom (S . (f,(id c9)))) by CAT_1:63 .= id (dom (T . f)) by FUNCT_5:70 ; ::_thesis: T . (id (cod f)) = id (cod (T . f)) thus T . (id (cod f)) = S . ((id (cod f)),(id c9)) by FUNCT_5:70 .= S . (id [(cod f),c9]) by Th31 .= S . (id [(cod f),(cod (id c9))]) .= S . (id (cod [f,(id c9)])) by Th28 .= id (cod (S . (f,(id c9)))) by CAT_1:63 .= id (cod (T . f)) by FUNCT_5:70 ; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) ) assume A3: dom g = cod f ; ::_thesis: T . (g (*) f) = (T . g) (*) (T . f) Hom (c9,c9) <> {} ; then A4: (id c9) * (id c9) = (id c9) (*) (id c9) by CAT_1:def_13; A5: ( dom [g,(id c9)] = [(dom g),(dom (id c9))] & cod [f,(id c9)] = [(cod f),(cod (id c9))] ) by Th28; thus T . (g (*) f) = S . ((g (*) f),((id c9) * (id c9))) by FUNCT_5:70 .= S . ([g,(id c9)] (*) [f,(id c9)]) by A3, A2, A4, Th29 .= (S . (g,(id c9))) (*) (S . (f,(id c9))) by A3, A5, CAT_1:64 .= (T . g) (*) (S . (f,(id c9))) by FUNCT_5:70 .= (T . g) (*) (T . f) by FUNCT_5:70 ; ::_thesis: verum end; hence (curry' S) . (id c9) is Functor of C,D by CAT_1:61; ::_thesis: verum end; definition let C, C9, D be Category; let S be Functor of [:C,C9:],D; let c be Object of C; funcS ?- c -> Functor of C9,D equals :: CAT_2:def 8 (curry S) . (id c); coherence (curry S) . (id c) is Functor of C9,D by Th34; end; :: deftheorem defines ?- CAT_2:def_8_:_ for C, C9, D being Category for S being Functor of [:C,C9:],D for c being Object of C holds S ?- c = (curry S) . (id c); theorem :: CAT_2:36 for C, C9, D being Category for S being Functor of [:C,C9:],D for c being Object of C for f being Morphism of C9 holds (S ?- c) . f = S . ((id c),f) by FUNCT_5:69; theorem :: CAT_2:37 for C, C9, D being Category for S being Functor of [:C,C9:],D for c being Object of C for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) proof let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D for c being Object of C for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) let S be Functor of [:C,C9:],D; ::_thesis: for c being Object of C for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) let c be Object of C; ::_thesis: for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) let c9 be Object of C9; ::_thesis: (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) (S ?- c) . (id c9) = S . ((id c),(id c9)) by FUNCT_5:69 .= S . (id [c,c9]) by Th31 .= id ((Obj S) . [c,c9]) by CAT_1:68 ; hence (Obj (S ?- c)) . c9 = (Obj S) . (c,c9) by CAT_1:67; ::_thesis: verum end; definition let C, C9, D be Category; let S be Functor of [:C,C9:],D; let c9 be Object of C9; funcS -? c9 -> Functor of C,D equals :: CAT_2:def 9 (curry' S) . (id c9); coherence (curry' S) . (id c9) is Functor of C,D by Th35; end; :: deftheorem defines -? CAT_2:def_9_:_ for C, C9, D being Category for S being Functor of [:C,C9:],D for c9 being Object of C9 holds S -? c9 = (curry' S) . (id c9); theorem :: CAT_2:38 for C, C9, D being Category for S being Functor of [:C,C9:],D for c9 being Object of C9 for f being Morphism of C holds (S -? c9) . f = S . (f,(id c9)) by FUNCT_5:70; theorem :: CAT_2:39 for C, C9, D being Category for S being Functor of [:C,C9:],D for c being Object of C for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9) proof let C, C9, D be Category; ::_thesis: for S being Functor of [:C,C9:],D for c being Object of C for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9) let S be Functor of [:C,C9:],D; ::_thesis: for c being Object of C for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9) let c be Object of C; ::_thesis: for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9) let c9 be Object of C9; ::_thesis: (Obj (S -? c9)) . c = (Obj S) . (c,c9) (S -? c9) . (id c) = S . ((id c),(id c9)) by FUNCT_5:70 .= S . (id [c,c9]) by Th31 .= id ((Obj S) . [c,c9]) by CAT_1:68 ; hence (Obj (S -? c9)) . c = (Obj S) . (c,c9) by CAT_1:67; ::_thesis: verum end; theorem :: CAT_2:40 for C, B, D being Category for L being Function of the carrier of C,(Funct (B,D)) for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) proof let C, B, D be Category; ::_thesis: for L being Function of the carrier of C,(Funct (B,D)) for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) deffunc H1( Category) -> set = the carrier' of \$1; let L be Function of the carrier of C,(Funct (B,D)); ::_thesis: for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) let M be Function of the carrier of B,(Funct (C,D)); ::_thesis: ( ( for c being Object of C for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) implies ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) assume that A1: for c being Object of C for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) and A2: for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ; ::_thesis: ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) deffunc H2( Element of H1(B), Element of H1(C)) -> Element of the carrier' of D = ((L . (cod \$2)) . \$1) (*) ((M . (dom \$1)) . \$2); consider S being Function of [:H1(B),H1(C):],H1(D) such that A3: for f being Morphism of B for g being Morphism of C holds S . (f,g) = H2(f,g) from BINOP_1:sch_4(); reconsider T = S as Function of H1([:B,C:]),H1(D) ; now__::_thesis:_(_(_for_bc_being_Object_of_[:B,C:]_ex_d_being_Object_of_D_st_T_._(id_bc)_=_id_d_)_&_(_for_fg_being_Morphism_of_[:B,C:]_holds_ (_T_._(id_(dom_fg))_=_id_(dom_(T_._fg))_&_T_._(id_(cod_fg))_=_id_(cod_(T_._fg))_)_)_&_(_for_fg1,_fg2_being_Morphism_of_[:B,C:]_st_dom_fg2_=_cod_fg1_holds_ T_._(fg2_(*)_fg1)_=_(T_._fg2)_(*)_(T_._fg1)_)_) thus for bc being Object of [:B,C:] ex d being Object of D st T . (id bc) = id d ::_thesis: ( ( for fg being Morphism of [:B,C:] holds ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) ) proof let bc be Object of [:B,C:]; ::_thesis: ex d being Object of D st T . (id bc) = id d consider b being Object of B, c being Object of C such that A4: bc = [b,c] by DOMAIN_1:1; consider d being Object of D such that A5: (L . c) . (id b) = id d by CAT_1:62; take d ; ::_thesis: T . (id bc) = id d Hom (d,d) <> {} ; then A6: (id d) * (id d) = (id d) (*) (id d) by CAT_1:def_13; A7: ( cod (id c) = c & dom (id b) = b ) ; (L . c) . (id b) = (M . b) . (id c) by A1; then T . ((id b),(id c)) = id d by A3, A5, A6, A7; hence T . (id bc) = id d by A4, Th31; ::_thesis: verum end; thus for fg being Morphism of [:B,C:] holds ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ::_thesis: for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) proof let fg be Morphism of [:B,C:]; ::_thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) consider f being Morphism of B, g being Morphism of C such that A8: fg = [f,g] by DOMAIN_1:1; set b = dom f; set c = dom g; set g9 = id (dom g); set f9 = id (dom f); A9: Hom ((dom ((M . (dom f)) . g)),(dom ((M . (dom f)) . g))) <> {} ; id (dom ((L . (cod g)) . f)) = (L . (cod g)) . (id (dom f)) by CAT_1:63 .= (M . (dom f)) . (id (cod g)) by A1 .= id (cod ((M . (dom f)) . g)) by CAT_1:63 ; then A10: dom ((L . (cod g)) . f) = cod ((M . (dom f)) . g) by CAT_1:59; thus T . (id (dom fg)) = S . (id [(dom f),(dom g)]) by A8, Th28 .= S . ((id (dom f)),(id (dom g))) by Th31 .= ((L . (cod (id (dom g)))) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g))) by A3 .= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g))) .= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom f)) . (id (dom g))) .= ((M . (dom f)) . (id (dom g))) (*) ((M . (dom f)) . (id (dom g))) by A1 .= (id (dom ((M . (dom f)) . g))) (*) ((M . (dom f)) . (id (dom g))) by CAT_1:63 .= (id (dom ((M . (dom f)) . g))) (*) (id (dom ((M . (dom f)) . g))) by CAT_1:63 .= (id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g))) by A9, CAT_1:def_13 .= id (dom (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17 .= id (dom (S . (f,g))) by A3 .= id (dom (T . fg)) by A8 ; ::_thesis: T . (id (cod fg)) = id (cod (T . fg)) set b = cod f; set c = cod g; set g9 = id (cod g); set f9 = id (cod f); A11: Hom ((cod ((L . (cod g)) . f)),(cod ((L . (cod g)) . f))) <> {} ; thus T . (id (cod fg)) = S . (id [(cod f),(cod g)]) by A8, Th28 .= S . ((id (cod f)),(id (cod g))) by Th31 .= ((L . (cod (id (cod g)))) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g))) by A3 .= ((L . (cod g)) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g))) .= ((L . (cod g)) . (id (cod f))) (*) ((M . (cod f)) . (id (cod g))) .= ((L . (cod g)) . (id (cod f))) (*) ((L . (cod g)) . (id (cod f))) by A1 .= (id (cod ((L . (cod g)) . f))) (*) ((L . (cod g)) . (id (cod f))) by CAT_1:63 .= (id (cod ((L . (cod g)) . f))) (*) (id (cod ((L . (cod g)) . f))) by CAT_1:63 .= (id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f))) by A11, CAT_1:def_13 .= id (cod (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17 .= id (cod (S . (f,g))) by A3 .= id (cod (T . fg)) by A8 ; ::_thesis: verum end; let fg1, fg2 be Morphism of [:B,C:]; ::_thesis: ( dom fg2 = cod fg1 implies T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) assume A12: dom fg2 = cod fg1 ; ::_thesis: T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) consider f1 being Morphism of B, g1 being Morphism of C such that A13: fg1 = [f1,g1] by DOMAIN_1:1; consider f2 being Morphism of B, g2 being Morphism of C such that A14: fg2 = [f2,g2] by DOMAIN_1:1; A15: [(cod f1),(cod g1)] = cod fg1 by A13, Th28; set L1 = L . (cod g1); set L2 = L . (cod g2); set M1 = M . (dom f1); set M2 = M . (dom f2); A16: [(dom f2),(dom g2)] = dom fg2 by A14, Th28; then A17: dom f2 = cod f1 by A12, A15, XTUPLE_0:1; then A18: dom ((L . (cod g2)) . f2) = cod ((L . (cod g2)) . f1) by CAT_1:64; id (dom ((L . (cod g1)) . f1)) = (L . (cod g1)) . (id (dom f1)) by CAT_1:63 .= (M . (dom f1)) . (id (cod g1)) by A1 .= id (cod ((M . (dom f1)) . g1)) by CAT_1:63 ; then A19: dom ((L . (cod g1)) . f1) = cod ((M . (dom f1)) . g1) by CAT_1:59; then A20: cod (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) = cod ((L . (cod g1)) . f1) by CAT_1:17; A21: dom g2 = cod g1 by A12, A16, A15, XTUPLE_0:1; then A22: dom ((M . (dom f1)) . g2) = cod ((M . (dom f1)) . g1) by CAT_1:64; then A23: cod (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) = cod ((M . (dom f1)) . g2) by CAT_1:17; id (dom ((M . (dom f2)) . g2)) = (M . (dom f2)) . (id (dom g2)) by CAT_1:63 .= (L . (cod g1)) . (id (cod f1)) by A1, A17, A21 .= id (cod ((L . (cod g1)) . f1)) by CAT_1:63 ; then A24: dom ((M . (dom f2)) . g2) = cod ((L . (cod g1)) . f1) by CAT_1:59; id (dom ((L . (cod g2)) . f2)) = (L . (cod g2)) . (id (dom f2)) by CAT_1:63 .= (M . (dom f2)) . (id (cod g2)) by A1 .= id (cod ((M . (dom f2)) . g2)) by CAT_1:63 ; then A25: dom ((L . (cod g2)) . f2) = cod ((M . (dom f2)) . g2) by CAT_1:59; set f = f2 (*) f1; set g = g2 (*) g1; id (dom ((L . (cod g2)) . f1)) = (L . (cod g2)) . (id (dom f1)) by CAT_1:63 .= (M . (dom f1)) . (id (cod g2)) by A1 .= id (cod ((M . (dom f1)) . g2)) by CAT_1:63 ; then A26: dom ((L . (cod g2)) . f1) = cod ((M . (dom f1)) . g2) by CAT_1:59; thus T . (fg2 (*) fg1) = S . ((f2 (*) f1),(g2 (*) g1)) by A12, A13, A14, Th30 .= ((L . (cod (g2 (*) g1))) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A3 .= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A21, CAT_1:17 .= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:17 .= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:64 .= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) by A21, CAT_1:64 .= ((L . (cod g2)) . f2) (*) (((L . (cod g2)) . f1) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1))) by A18, A23, A26, CAT_1:18 .= ((L . (cod g2)) . f2) (*) ((((L . (cod g2)) . f1) (*) ((M . (dom f1)) . g2)) (*) ((M . (dom f1)) . g1)) by A22, A26, CAT_1:18 .= ((L . (cod g2)) . f2) (*) ((((M . (dom f2)) . g2) (*) ((L . (cod g1)) . f1)) (*) ((M . (dom f1)) . g1)) by A2, A17, A21 .= ((L . (cod g2)) . f2) (*) (((M . (dom f2)) . g2) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1))) by A19, A24, CAT_1:18 .= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) by A24, A25, A20, CAT_1:18 .= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (S . (f1,g1)) by A3 .= (S . (f2,g2)) (*) (T . fg1) by A3, A13 .= (T . fg2) (*) (T . fg1) by A14 ; ::_thesis: verum end; then reconsider T = T as Functor of [:B,C:],D by CAT_1:61; take T ; ::_thesis: for f being Morphism of B for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) thus for f being Morphism of B for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A3; ::_thesis: verum end; theorem :: CAT_2:41 for C, B, D being Category for L being Function of the carrier of C,(Funct (B,D)) for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st for c being Object of C for b being Object of B holds ( S -? c = L . c & S ?- b = M . b ) holds for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) proof let C, B, D be Category; ::_thesis: for L being Function of the carrier of C,(Funct (B,D)) for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st for c being Object of C for b being Object of B holds ( S -? c = L . c & S ?- b = M . b ) holds for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) let L be Function of the carrier of C,(Funct (B,D)); ::_thesis: for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st for c being Object of C for b being Object of B holds ( S -? c = L . c & S ?- b = M . b ) holds for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) let M be Function of the carrier of B,(Funct (C,D)); ::_thesis: ( ex S being Functor of [:B,C:],D st for c being Object of C for b being Object of B holds ( S -? c = L . c & S ?- b = M . b ) implies for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) given S being Functor of [:B,C:],D such that A1: for c being Object of C for b being Object of B holds ( S -? c = L . c & S ?- b = M . b ) ; ::_thesis: for f being Morphism of B for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) let f be Morphism of B; ::_thesis: for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) let g be Morphism of C; ::_thesis: ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) dom (id (cod f)) = cod f ; then A2: dom [(id (cod f)),g] = [(cod f),(dom g)] by Th28; cod (id (dom g)) = dom g ; then A3: cod [f,(id (dom g))] = [(cod f),(dom g)] by Th28; cod (id (dom f)) = dom f ; then A4: cod [(id (dom f)),g] = [(dom f),(cod g)] by Th28; dom (id (cod g)) = cod g ; then A5: dom [f,(id (cod g))] = [(dom f),(cod g)] by Th28; thus ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((S ?- (cod f)) . g) (*) ((L . (dom g)) . f) by A1 .= ((S ?- (cod f)) . g) (*) ((S -? (dom g)) . f) by A1 .= (S . ((id (cod f)),g)) (*) ((S -? (dom g)) . f) by FUNCT_5:69 .= (S . ((id (cod f)),g)) (*) (S . (f,(id (dom g)))) by FUNCT_5:70 .= S . ([(id (cod f)),g] (*) [f,(id (dom g))]) by A2, A3, CAT_1:64 .= S . [((id (cod f)) (*) f),(g (*) (id (dom g)))] by A2, A3, Th30 .= S . [f,(g (*) (id (dom g)))] by CAT_1:21 .= S . [f,g] by CAT_1:22 .= S . [(f (*) (id (dom f))),g] by CAT_1:22 .= S . [(f (*) (id (dom f))),((id (cod g)) (*) g)] by CAT_1:21 .= S . ([f,(id (cod g))] (*) [(id (dom f)),g]) by A5, A4, Th30 .= (S . (f,(id (cod g)))) (*) (S . [(id (dom f)),g]) by A5, A4, CAT_1:64 .= ((S -? (cod g)) . f) (*) (S . ((id (dom f)),g)) by FUNCT_5:70 .= ((S -? (cod g)) . f) (*) ((S ?- (dom f)) . g) by FUNCT_5:69 .= ((L . (cod g)) . f) (*) ((S ?- (dom f)) . g) by A1 .= ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A1 ; ::_thesis: verum end; definition let C, D be Category; func pr1 (C,D) -> Functor of [:C,D:],C equals :: CAT_2:def 10 pr1 ( the carrier' of C, the carrier' of D); coherence pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C proof reconsider T = pr1 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of C ; now__::_thesis:_(_(_for_cd_being_Object_of_[:C,D:]_ex_c_being_Object_of_C_st_T_._(id_cd)_=_id_c_)_&_(_for_fg_being_Morphism_of_[:C,D:]_holds_ (_T_._(id_(dom_fg))_=_id_(dom_(T_._fg))_&_T_._(id_(cod_fg))_=_id_(cod_(T_._fg))_)_)_&_(_for_fg,_fg9_being_Morphism_of_[:C,D:]_st_dom_fg9_=_cod_fg_holds_ T_._(fg9_(*)_fg)_=_(T_._fg9)_(*)_(T_._fg)_)_) thus for cd being Object of [:C,D:] ex c being Object of C st T . (id cd) = id c ::_thesis: ( ( for fg being Morphism of [:C,D:] holds ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) ) proof let cd be Object of [:C,D:]; ::_thesis: ex c being Object of C st T . (id cd) = id c consider c being Object of C, d being Object of D such that A1: cd = [c,d] by DOMAIN_1:1; A2: T . ((id c),(id d)) = id c by FUNCT_3:def_4; id cd = [(id c),(id d)] by A1, Th31; hence ex c being Object of C st T . (id cd) = id c by A2; ::_thesis: verum end; thus for fg being Morphism of [:C,D:] holds ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ::_thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) proof let fg be Morphism of [:C,D:]; ::_thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) consider f being Morphism of C, g being Morphism of D such that A3: fg = [f,g] by DOMAIN_1:1; T . (f,g) = T . fg by A3; then A4: T . fg = f by FUNCT_3:def_4; dom [f,g] = [(dom f),(dom g)] by Th28; hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A3, Th31 .= id (dom (T . fg)) by A4, FUNCT_3:def_4 ; ::_thesis: T . (id (cod fg)) = id (cod (T . fg)) cod [f,g] = [(cod f),(cod g)] by Th28; hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A3, Th31 .= id (cod (T . fg)) by A4, FUNCT_3:def_4 ; ::_thesis: verum end; let fg, fg9 be Morphism of [:C,D:]; ::_thesis: ( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) assume A5: dom fg9 = cod fg ; ::_thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) consider f being Morphism of C, g being Morphism of D such that A6: fg = [f,g] by DOMAIN_1:1; T . (f,g) = T . fg by A6; then A7: T . fg = f by FUNCT_3:def_4; consider f9 being Morphism of C, g9 being Morphism of D such that A8: fg9 = [f9,g9] by DOMAIN_1:1; T . (f9,g9) = T . fg9 by A8; then A9: T . fg9 = f9 by FUNCT_3:def_4; ( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th28; then ( dom f9 = cod f & dom g9 = cod g ) by A5, A6, A8, XTUPLE_0:1; hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A6, A8, Th29 .= (T . fg9) (*) (T . fg) by A9, A7, FUNCT_3:def_4 ; ::_thesis: verum end; hence pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C by CAT_1:61; ::_thesis: verum end; func pr2 (C,D) -> Functor of [:C,D:],D equals :: CAT_2:def 11 pr2 ( the carrier' of C, the carrier' of D); coherence pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D proof reconsider T = pr2 ( the carrier' of C, the carrier' of D) as Function of the carrier' of [:C,D:], the carrier' of D ; now__::_thesis:_(_(_for_cd_being_Object_of_[:C,D:]_ex_d_being_Object_of_D_st_T_._(id_cd)_=_id_d_)_&_(_for_fg_being_Morphism_of_[:C,D:]_holds_ (_T_._(id_(dom_fg))_=_id_(dom_(T_._fg))_&_T_._(id_(cod_fg))_=_id_(cod_(T_._fg))_)_)_&_(_for_fg,_fg9_being_Morphism_of_[:C,D:]_st_dom_fg9_=_cod_fg_holds_ T_._(fg9_(*)_fg)_=_(T_._fg9)_(*)_(T_._fg)_)_) thus for cd being Object of [:C,D:] ex d being Object of D st T . (id cd) = id d ::_thesis: ( ( for fg being Morphism of [:C,D:] holds ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) ) proof let cd be Object of [:C,D:]; ::_thesis: ex d being Object of D st T . (id cd) = id d consider c being Object of C, d being Object of D such that A10: cd = [c,d] by DOMAIN_1:1; A11: T . ((id c),(id d)) = id d by FUNCT_3:def_5; id cd = [(id c),(id d)] by A10, Th31; hence ex d being Object of D st T . (id cd) = id d by A11; ::_thesis: verum end; thus for fg being Morphism of [:C,D:] holds ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ::_thesis: for fg, fg9 being Morphism of [:C,D:] st dom fg9 = cod fg holds T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) proof let fg be Morphism of [:C,D:]; ::_thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) consider f being Morphism of C, g being Morphism of D such that A12: fg = [f,g] by DOMAIN_1:1; T . (f,g) = T . fg by A12; then A13: T . fg = g by FUNCT_3:def_5; dom [f,g] = [(dom f),(dom g)] by Th28; hence T . (id (dom fg)) = T . ((id (dom f)),(id (dom g))) by A12, Th31 .= id (dom (T . fg)) by A13, FUNCT_3:def_5 ; ::_thesis: T . (id (cod fg)) = id (cod (T . fg)) cod [f,g] = [(cod f),(cod g)] by Th28; hence T . (id (cod fg)) = T . ((id (cod f)),(id (cod g))) by A12, Th31 .= id (cod (T . fg)) by A13, FUNCT_3:def_5 ; ::_thesis: verum end; let fg, fg9 be Morphism of [:C,D:]; ::_thesis: ( dom fg9 = cod fg implies T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) ) assume A14: dom fg9 = cod fg ; ::_thesis: T . (fg9 (*) fg) = (T . fg9) (*) (T . fg) consider f being Morphism of C, g being Morphism of D such that A15: fg = [f,g] by DOMAIN_1:1; T . (f,g) = T . fg by A15; then A16: T . fg = g by FUNCT_3:def_5; consider f9 being Morphism of C, g9 being Morphism of D such that A17: fg9 = [f9,g9] by DOMAIN_1:1; T . (f9,g9) = T . fg9 by A17; then A18: T . fg9 = g9 by FUNCT_3:def_5; ( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th28; then ( dom f9 = cod f & dom g9 = cod g ) by A14, A15, A17, XTUPLE_0:1; hence T . (fg9 (*) fg) = T . ((f9 (*) f),(g9 (*) g)) by A15, A17, Th29 .= (T . fg9) (*) (T . fg) by A18, A16, FUNCT_3:def_5 ; ::_thesis: verum end; hence pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D by CAT_1:61; ::_thesis: verum end; end; :: deftheorem defines pr1 CAT_2:def_10_:_ for C, D being Category holds pr1 (C,D) = pr1 ( the carrier' of C, the carrier' of D); :: deftheorem defines pr2 CAT_2:def_11_:_ for C, D being Category holds pr2 (C,D) = pr2 ( the carrier' of C, the carrier' of D); theorem :: CAT_2:42 canceled; theorem :: CAT_2:43 canceled; theorem :: CAT_2:44 for C, D being Category for c being Object of C for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c proof let C, D be Category; ::_thesis: for c being Object of C for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c let c be Object of C; ::_thesis: for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c let d be Object of D; ::_thesis: (Obj (pr1 (C,D))) . (c,d) = c ( id [c,d] = [(id c),(id d)] & (pr1 (C,D)) . ((id c),(id d)) = id c ) by Th31, FUNCT_3:def_4; hence (Obj (pr1 (C,D))) . (c,d) = c by CAT_1:67; ::_thesis: verum end; theorem :: CAT_2:45 for C, D being Category for c being Object of C for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d proof let C, D be Category; ::_thesis: for c being Object of C for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d let c be Object of C; ::_thesis: for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d let d be Object of D; ::_thesis: (Obj (pr2 (C,D))) . (c,d) = d ( id [c,d] = [(id c),(id d)] & (pr2 (C,D)) . ((id c),(id d)) = id d ) by Th31, FUNCT_3:def_5; hence (Obj (pr2 (C,D))) . (c,d) = d by CAT_1:67; ::_thesis: verum end; definition let C, D, D9 be Category; let T be Functor of C,D; let T9 be Functor of C,D9; :: original: <: redefine func<:T,T9:> -> Functor of C,[:D,D9:]; coherence <:T,T9:> is Functor of C,[:D,D9:] proof reconsider S = <:T,T9:> as Function of the carrier' of C, the carrier' of [:D,D9:] ; now__::_thesis:_(_(_for_c_being_Object_of_C_ex_dd9_being_Object_of_[:D,D9:]_st_S_._(id_c)_=_id_dd9_)_&_(_for_f_being_Morphism_of_C_holds_ (_S_._(id_(dom_f))_=_id_(dom_(S_._f))_&_S_._(id_(cod_f))_=_id_(cod_(S_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ S_._(g_(*)_f)_=_(S_._g)_(*)_(S_._f)_)_) thus for c being Object of C ex dd9 being Object of [:D,D9:] st S . (id c) = id dd9 ::_thesis: ( ( for f being Morphism of C holds ( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds S . (g (*) f) = (S . g) (*) (S . f) ) ) proof let c be Object of C; ::_thesis: ex dd9 being Object of [:D,D9:] st S . (id c) = id dd9 set d = (Obj T) . c; set d9 = (Obj T9) . c; take dd9 = [((Obj T) . c),((Obj T9) . c)]; ::_thesis: S . (id c) = id dd9 thus S . (id c) = [(T . (id c)),(T9 . (id c))] by FUNCT_3:59 .= [(id ((Obj T) . c)),(T9 . (id c))] by CAT_1:68 .= [(id ((Obj T) . c)),(id ((Obj T9) . c))] by CAT_1:68 .= id dd9 by Th31 ; ::_thesis: verum end; thus for f being Morphism of C holds ( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds S . (g (*) f) = (S . g) (*) (S . f) proof let f be Morphism of C; ::_thesis: ( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ( T . (id (dom f)) = id (dom (T . f)) & T9 . (id (dom f)) = id (dom (T9 . f)) ) by CAT_1:63; hence S . (id (dom f)) = [(id (dom (T . f))),(id (dom (T9 . f)))] by FUNCT_3:59 .= id [(dom (T . f)),(dom (T9 . f))] by Th31 .= id (dom [(T . f),(T9 . f)]) by Th28 .= id (dom (S . f)) by FUNCT_3:59 ; ::_thesis: S . (id (cod f)) = id (cod (S . f)) ( T . (id (cod f)) = id (cod (T . f)) & T9 . (id (cod f)) = id (cod (T9 . f)) ) by CAT_1:63; hence S . (id (cod f)) = [(id (cod (T . f))),(id (cod (T9 . f)))] by FUNCT_3:59 .= id [(cod (T . f)),(cod (T9 . f))] by Th31 .= id (cod [(T . f),(T9 . f)]) by Th28 .= id (cod (S . f)) by FUNCT_3:59 ; ::_thesis: verum end; let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies S . (g (*) f) = (S . g) (*) (S . f) ) assume A1: dom g = cod f ; ::_thesis: S . (g (*) f) = (S . g) (*) (S . f) then A2: ( dom (T . g) = cod (T . f) & dom (T9 . g) = cod (T9 . f) ) by CAT_1:64; ( T . (g (*) f) = (T . g) (*) (T . f) & T9 . (g (*) f) = (T9 . g) (*) (T9 . f) ) by A1, CAT_1:64; hence S . (g (*) f) = [((T . g) (*) (T . f)),((T9 . g) (*) (T9 . f))] by FUNCT_3:59 .= [(T . g),(T9 . g)] (*) [(T . f),(T9 . f)] by A2, Th29 .= (S . g) (*) [(T . f),(T9 . f)] by FUNCT_3:59 .= (S . g) (*) (S . f) by FUNCT_3:59 ; ::_thesis: verum end; hence <:T,T9:> is Functor of C,[:D,D9:] by CAT_1:61; ::_thesis: verum end; end; theorem :: CAT_2:46 canceled; theorem :: CAT_2:47 for C, D, D9 being Category for T being Functor of C,D for T9 being Functor of C,D9 for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] proof let C, D, D9 be Category; ::_thesis: for T being Functor of C,D for T9 being Functor of C,D9 for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] let T be Functor of C,D; ::_thesis: for T9 being Functor of C,D9 for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] let T9 be Functor of C,D9; ::_thesis: for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] let c be Object of C; ::_thesis: (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] A1: ( T . (id c) = id ((Obj T) . c) & T9 . (id c) = id ((Obj T9) . c) ) by CAT_1:68; ( <:T,T9:> . (id c) = [(T . (id c)),(T9 . (id c))] & [(id ((Obj T) . c)),(id ((Obj T9) . c))] = id [((Obj T) . c),((Obj T9) . c)] ) by Th31, FUNCT_3:59; hence (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] by A1, CAT_1:67; ::_thesis: verum end; theorem Th48: :: CAT_2:48 for C, D, C9, D9 being Category for T being Functor of C,D for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> proof let C, D, C9, D9 be Category; ::_thesis: for T being Functor of C,D for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> let T be Functor of C,D; ::_thesis: for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> let T9 be Functor of C9,D9; ::_thesis: [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> ( dom T = the carrier' of C & dom T9 = the carrier' of C9 ) by FUNCT_2:def_1; hence [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> by FUNCT_3:66; ::_thesis: verum end; definition let C, C9, D, D9 be Category; let T be Functor of C,D; let T9 be Functor of C9,D9; :: original: [: redefine func[:T,T9:] -> Functor of [:C,C9:],[:D,D9:]; coherence [:T,T9:] is Functor of [:C,C9:],[:D,D9:] proof [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):> by Th48; hence [:T,T9:] is Functor of [:C,C9:],[:D,D9:] ; ::_thesis: verum end; end; theorem :: CAT_2:49 canceled; theorem :: CAT_2:50 for C, D, C9, D9 being Category for T being Functor of C,D for T9 being Functor of C9,D9 for c being Object of C for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] proof let C, D, C9, D9 be Category; ::_thesis: for T being Functor of C,D for T9 being Functor of C9,D9 for c being Object of C for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] let T be Functor of C,D; ::_thesis: for T9 being Functor of C9,D9 for c being Object of C for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] let T9 be Functor of C9,D9; ::_thesis: for c being Object of C for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] let c be Object of C; ::_thesis: for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] let c9 be Object of C9; ::_thesis: (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] A1: ( T . (id c) = id ((Obj T) . c) & T9 . (id c9) = id ((Obj T9) . c9) ) by CAT_1:68; A2: [(id ((Obj T) . c)),(id ((Obj T9) . c9))] = id [((Obj T) . c),((Obj T9) . c9)] by Th31; ( [:T,T9:] . ((id c),(id c9)) = [(T . (id c)),(T9 . (id c9))] & [(id c),(id c9)] = id [c,c9] ) by Th31, FUNCT_3:75; hence (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)] by A1, A2, CAT_1:67; ::_thesis: verum end;