:: COMMACAT semantic presentation begin deffunc H1( CatStr ) -> set = the carrier of \$1; deffunc H2( CatStr ) -> set = the carrier' of \$1; definition let C, D, E be Category; let F be Functor of C,E; let G be Functor of D,E; given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ; func commaObjs (F,G) -> non empty Subset of [:[: the carrier of C, the carrier of D:], the carrier' of E:] equals :Def1: :: COMMACAT:def 1 { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } ; coherence { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } is non empty Subset of [:[: the carrier of C, the carrier of D:], the carrier' of E:] proof A2: { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } c= [:[: the carrier of C, the carrier of D:], the carrier' of E:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } or x in [:[: the carrier of C, the carrier of D:], the carrier' of E:] ) assume x in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } ; ::_thesis: x in [:[: the carrier of C, the carrier of D:], the carrier' of E:] then ex c being Object of C ex d being Object of D ex f being Morphism of E st ( x = [[c,d],f] & f in Hom ((F . c),(G . d)) ) ; hence x in [:[: the carrier of C, the carrier of D:], the carrier' of E:] ; ::_thesis: verum end; [[c1,d1],f1] in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } by A1; hence { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } is non empty Subset of [:[: the carrier of C, the carrier of D:], the carrier' of E:] by A2; ::_thesis: verum end; end; :: deftheorem Def1 defines commaObjs COMMACAT:def_1_:_ for C, D, E being Category for F being Functor of C,E for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds commaObjs (F,G) = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } ; theorem Th1: :: COMMACAT:1 for C, D, E being Category for F being Functor of C,E for G being Functor of D,E for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) proof let C, D, E be Category; ::_thesis: for F being Functor of C,E for G being Functor of D,E for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) let F be Functor of C,E; ::_thesis: for G being Functor of D,E for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) let G be Functor of D,E; ::_thesis: for o being Element of commaObjs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) let o be Element of commaObjs (F,G); ::_thesis: ( ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) implies ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) ) assume ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) ; ::_thesis: ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) then A1: commaObjs (F,G) = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } by Def1; o in commaObjs (F,G) ; then consider c being Object of C, d being Object of D, f being Morphism of E such that A2: o = [[c,d],f] and A3: f in Hom ((F . c),(G . d)) by A1; A4: o `2 = f by A2, MCART_1:7; ( o `11 = c & o `12 = d ) by A2, MCART_1:85; hence ( o = [[(o `11),(o `12)],(o `2)] & o `2 in Hom ((F . (o `11)),(G . (o `12))) & dom (o `2) = F . (o `11) & cod (o `2) = G . (o `12) ) by A2, A3, A4, CAT_1:1; ::_thesis: verum end; definition let C, D, E be Category; let F be Functor of C,E; let G be Functor of D,E; given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ; func commaMorphs (F,G) -> non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] equals :Def2: :: COMMACAT:def 2 { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } ; coherence { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } is non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] proof commaObjs (F,G) = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } by A1, Def1; then [[c1,d1],f1] in commaObjs (F,G) by A1; then reconsider o = [[c1,d1],f1] as Element of commaObjs (F,G) ; set X = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } ; A2: ( dom (id d1) = d1 & cod (id d1) = d1 ) ; A3: ( (o `1) `1 = o `11 & (o `1) `2 = o `12 ) by MCART_1:def_14, MCART_1:def_15; A4: { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } c= [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } or x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] ) assume x in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } ; ::_thesis: x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] then ex g being Morphism of C ex h being Morphism of D ex o1, o2 being Element of commaObjs (F,G) st ( x = [[o1,o2],[g,h]] & dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) ; hence x in [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] ; ::_thesis: verum end; A5: ( [c1,d1] `2 = d1 & o `2 = f1 ) by MCART_1:7; A6: ( o `1 = [c1,d1] & [c1,d1] `1 = c1 ) by MCART_1:7; cod f1 = G . d1 by A1, CAT_1:1; then A7: (id (G . d1)) (*) f1 = f1 by CAT_1:21; dom f1 = F . c1 by A1, CAT_1:1; then A8: f1 (*) (id (F . c1)) = f1 by CAT_1:22; A9: ( F . (id c1) = id (F . c1) & G . (id d1) = id (G . d1) ) by CAT_1:71; ( dom (id c1) = c1 & cod (id c1) = c1 ) ; then [[o,o],[(id c1),(id d1)]] in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } by A2, A3, A6, A5, A8, A7, A9; hence { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } is non empty Subset of [:[:(commaObjs (F,G)),(commaObjs (F,G)):],[: the carrier' of C, the carrier' of D:]:] by A4; ::_thesis: verum end; end; :: deftheorem Def2 defines commaMorphs COMMACAT:def_2_:_ for C, D, E being Category for F being Functor of C,E for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds commaMorphs (F,G) = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } ; definition let C, D, E be Category; let F be Functor of C,E; let G be Functor of D,E; let k be Element of commaMorphs (F,G); :: original: `11 redefine funck `11 -> Element of commaObjs (F,G); coherence k `11 is Element of commaObjs (F,G) proof thus k `11 is Element of commaObjs (F,G) ; ::_thesis: verum end; :: original: `12 redefine funck `12 -> Element of commaObjs (F,G); coherence k `12 is Element of commaObjs (F,G) proof thus k `12 is Element of commaObjs (F,G) ; ::_thesis: verum end; end; theorem Th2: :: COMMACAT:2 for C, D, E being Category for F being Functor of C,E for G being Functor of D,E for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) proof let C, D, E be Category; ::_thesis: for F being Functor of C,E for G being Functor of D,E for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) let F be Functor of C,E; ::_thesis: for G being Functor of D,E for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) let G be Functor of D,E; ::_thesis: for k being Element of commaMorphs (F,G) st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) holds ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) let k be Element of commaMorphs (F,G); ::_thesis: ( ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) implies ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) ) assume ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom ((F . c),(G . d)) ; ::_thesis: ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) then A1: commaMorphs (F,G) = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } by Def2; k in commaMorphs (F,G) ; then consider g being Morphism of C, h being Morphism of D, o1, o2 being Element of commaObjs (F,G) such that A2: k = [[o1,o2],[g,h]] and A3: ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) by A1; A4: k `21 = g by A2, MCART_1:85; ( k `11 = o1 & k `12 = o2 ) by A2, MCART_1:85; hence ( k = [[(k `11),(k `12)],[(k `21),(k `22)]] & dom (k `21) = (k `11) `11 & cod (k `21) = (k `12) `11 & dom (k `22) = (k `11) `12 & cod (k `22) = (k `12) `12 & ((k `12) `2) (*) (F . (k `21)) = (G . (k `22)) (*) ((k `11) `2) ) by A2, A3, A4, MCART_1:85; ::_thesis: verum end; definition let C, D, E be Category; let F be Functor of C,E; let G be Functor of D,E; let k1, k2 be Element of commaMorphs (F,G); given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ; assume A2: k1 `12 = k2 `11 ; funck2 * k1 -> Element of commaMorphs (F,G) equals :Def3: :: COMMACAT:def 3 [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]; coherence [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is Element of commaMorphs (F,G) proof set k22 = (k2 `22) (*) (k1 `22); set k21 = (k2 `21) (*) (k1 `21); A3: ( F . (cod (k2 `21)) = cod (F . (k2 `21)) & dom (F . (k2 `21)) = F . (dom (k2 `21)) ) by CAT_1:72; A4: cod (F . (k1 `21)) = F . (cod (k1 `21)) by CAT_1:72; A5: cod ((k1 `12) `2) = G . ((k1 `12) `12) by A1, Th1; A6: dom (k1 `22) = (k1 `11) `12 by A1, Th2; A7: ( ((k2 `12) `2) (*) (F . (k2 `21)) = (G . (k2 `22)) (*) ((k2 `11) `2) & dom ((k2 `12) `2) = F . ((k2 `12) `11) ) by A1, Th1, Th2; A8: cod (G . (k1 `22)) = G . (cod (k1 `22)) by CAT_1:72; A9: ( ((k1 `12) `2) (*) (F . (k1 `21)) = (G . (k1 `22)) (*) ((k1 `11) `2) & dom ((k1 `12) `2) = F . ((k1 `12) `11) ) by A1, Th1, Th2; A10: dom (G . (k2 `22)) = G . (dom (k2 `22)) by CAT_1:72; A11: ( cod ((k1 `11) `2) = G . ((k1 `11) `12) & dom (G . (k1 `22)) = G . (dom (k1 `22)) ) by A1, Th1, CAT_1:72; A12: cod (k2 `21) = (k2 `12) `11 by A1, Th2; A13: commaMorphs (F,G) = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) (*) (F . g) = (G . h) (*) (o1 `2) ) } by A1, Def2; A14: dom (k2 `22) = (k2 `11) `12 by A1, Th2; A15: cod (k1 `22) = (k1 `12) `12 by A1, Th2; then A16: ( dom ((k2 `22) (*) (k1 `22)) = dom (k1 `22) & cod ((k2 `22) (*) (k1 `22)) = cod (k2 `22) ) by A2, A14, CAT_1:17; A17: ( dom (k1 `21) = (k1 `11) `11 & cod (k2 `22) = (k2 `12) `12 ) by A1, Th2; A18: cod (k1 `21) = (k1 `12) `11 by A1, Th2; A19: dom (k2 `21) = (k2 `11) `11 by A1, Th2; then A20: ( dom ((k2 `21) (*) (k1 `21)) = dom (k1 `21) & cod ((k2 `21) (*) (k1 `21)) = cod (k2 `21) ) by A2, A18, CAT_1:17; ((k2 `12) `2) (*) (F . ((k2 `21) (*) (k1 `21))) = ((k2 `12) `2) (*) ((F . (k2 `21)) (*) (F . (k1 `21))) by A2, A18, A19, CAT_1:64 .= ((G . (k2 `22)) (*) ((k2 `11) `2)) (*) (F . (k1 `21)) by A2, A18, A19, A12, A7, A3, A4, CAT_1:18 .= (G . (k2 `22)) (*) ((G . (k1 `22)) (*) ((k1 `11) `2)) by A2, A18, A14, A9, A5, A4, A10, CAT_1:18 .= ((G . (k2 `22)) (*) (G . (k1 `22))) (*) ((k1 `11) `2) by A2, A6, A15, A14, A10, A11, A8, CAT_1:18 .= (G . ((k2 `22) (*) (k1 `22))) (*) ((k1 `11) `2) by A2, A15, A14, CAT_1:64 ; then [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] in commaMorphs (F,G) by A6, A12, A17, A13, A20, A16; hence [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is Element of commaMorphs (F,G) ; ::_thesis: verum end; end; :: deftheorem Def3 defines * COMMACAT:def_3_:_ for C, D, E being Category for F being Functor of C,E for G being Functor of D,E for k1, k2 being Element of commaMorphs (F,G) st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) & k1 `12 = k2 `11 holds k2 * k1 = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]; definition let C, D, E be Category; let F be Functor of C,E; let G be Functor of D,E; func commaComp (F,G) -> PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) means :Def4: :: COMMACAT:def 4 ( dom it = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom it holds it . [k,k9] = k * k9 ) ); existence ex b1 being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) st ( dom b1 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b1 holds b1 . [k,k9] = k * k9 ) ) proof defpred S1[ set , set ] means ex k1, k2 being Element of commaMorphs (F,G) st ( \$1 = [k1,k2] & \$2 = k1 * k2 ); set X = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } ; A1: for x being set st x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } implies ex y being set st S1[x,y] ) assume x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } ; ::_thesis: ex y being set st S1[x,y] then consider k1, k2 being Element of commaMorphs (F,G) such that A2: x = [k1,k2] and k1 `11 = k2 `12 ; reconsider y = k1 * k2 as set ; take y ; ::_thesis: S1[x,y] take k1 ; ::_thesis: ex k2 being Element of commaMorphs (F,G) st ( x = [k1,k2] & y = k1 * k2 ) take k2 ; ::_thesis: ( x = [k1,k2] & y = k1 * k2 ) thus ( x = [k1,k2] & y = k1 * k2 ) by A2; ::_thesis: verum end; consider f being Function such that A3: ( dom f = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for x being set st x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); A4: rng f c= commaMorphs (F,G) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in commaMorphs (F,G) ) assume x in rng f ; ::_thesis: x in commaMorphs (F,G) then consider y being set such that A5: y in dom f and A6: x = f . y by FUNCT_1:def_3; ex k1, k2 being Element of commaMorphs (F,G) st ( y = [k1,k2] & f . y = k1 * k2 ) by A3, A5; hence x in commaMorphs (F,G) by A6; ::_thesis: verum end; dom f c= [:(commaMorphs (F,G)),(commaMorphs (F,G)):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] ) assume x in dom f ; ::_thesis: x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] then ex k1, k2 being Element of commaMorphs (F,G) st ( x = [k1,k2] & k1 `11 = k2 `12 ) by A3; hence x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] ; ::_thesis: verum end; then reconsider f = f as PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) by A4, RELSET_1:4; take f ; ::_thesis: ( dom f = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f holds f . [k,k9] = k * k9 ) ) thus dom f = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } by A3; ::_thesis: for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f holds f . [k,k9] = k * k9 let k1, k2 be Element of commaMorphs (F,G); ::_thesis: ( [k1,k2] in dom f implies f . [k1,k2] = k1 * k2 ) assume [k1,k2] in dom f ; ::_thesis: f . [k1,k2] = k1 * k2 then consider k, k9 being Element of commaMorphs (F,G) such that A7: [k1,k2] = [k,k9] and A8: f . [k1,k2] = k * k9 by A3; k1 = k by A7, XTUPLE_0:1; hence f . [k1,k2] = k1 * k2 by A7, A8, XTUPLE_0:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) st dom b1 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b1 holds b1 . [k,k9] = k * k9 ) & dom b2 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b2 holds b2 . [k,k9] = k * k9 ) holds b1 = b2 proof let f1, f2 be PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)); ::_thesis: ( dom f1 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f1 holds f1 . [k,k9] = k * k9 ) & dom f2 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f2 holds f2 . [k,k9] = k * k9 ) implies f1 = f2 ) assume that A9: ( dom f1 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f1 holds f1 . [k,k9] = k * k9 ) ) and A10: ( dom f2 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f2 holds f2 . [k,k9] = k * k9 ) ) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in__{__[k1,k2]_where_k1,_k2_is_Element_of_commaMorphs_(F,G)_:_k1_`11_=_k2_`12__}__holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } implies f1 . x = f2 . x ) assume A11: x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } ; ::_thesis: f1 . x = f2 . x then consider k1, k2 being Element of commaMorphs (F,G) such that A12: x = [k1,k2] and k1 `11 = k2 `12 ; thus f1 . x = k1 * k2 by A9, A11, A12 .= f2 . x by A10, A11, A12 ; ::_thesis: verum end; hence f1 = f2 by A9, A10, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines commaComp COMMACAT:def_4_:_ for C, D, E being Category for F being Functor of C,E for G being Functor of D,E for b6 being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) holds ( b6 = commaComp (F,G) iff ( dom b6 = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b6 holds b6 . [k,k9] = k * k9 ) ) ); definition let C, D, E be Category; let F be Functor of C,E; let G be Functor of D,E; given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom ((F . c1),(G . d1)) ; funcF comma G -> strict Category means :: COMMACAT:def 5 ( the carrier of it = commaObjs (F,G) & the carrier' of it = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of it . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of it . k = k `12 ) & the Comp of it = commaComp (F,G) ); existence ex b1 being strict Category st ( the carrier of b1 = commaObjs (F,G) & the carrier' of b1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b1 . k = k `12 ) & the Comp of b1 = commaComp (F,G) ) proof reconsider O = commaObjs (F,G), M = commaMorphs (F,G) as non empty set ; defpred S1[ Element of commaObjs (F,G), set ] means \$2 = [[\$1,\$1],[(id (\$1 `11)),(id (\$1 `12))]]; deffunc H3( Element of commaMorphs (F,G)) -> Element of commaObjs (F,G) = \$1 `12 ; deffunc H4( Element of commaMorphs (F,G)) -> Element of commaObjs (F,G) = \$1 `11 ; consider D9 being Function of (commaMorphs (F,G)),(commaObjs (F,G)) such that A2: for k being Element of commaMorphs (F,G) holds D9 . k = H4(k) from FUNCT_2:sch_4(); set I = the Function of (commaObjs (F,G)),(commaMorphs (F,G)); reconsider I = the Function of (commaObjs (F,G)),(commaMorphs (F,G)) as Function of O,M ; reconsider a9 = commaComp (F,G) as PartFunc of [:M,M:],M ; consider C9 being Function of (commaMorphs (F,G)),(commaObjs (F,G)) such that A3: for k being Element of commaMorphs (F,G) holds C9 . k = H3(k) from FUNCT_2:sch_4(); reconsider D9 = D9, C9 = C9 as Function of M,O ; set FG = CatStr(# O,M,D9,C9,a9 #); A4: dom the Comp of CatStr(# O,M,D9,C9,a9 #) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } by Def4; A5: for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) for k1, k2 being Element of commaMorphs (F,G) st f = k1 & g = k2 & dom g = cod f holds g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] proof let f, g be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: for k1, k2 being Element of commaMorphs (F,G) st f = k1 & g = k2 & dom g = cod f holds g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] let k1, k2 be Element of commaMorphs (F,G); ::_thesis: ( f = k1 & g = k2 & dom g = cod f implies g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] ) assume that A6: ( f = k1 & g = k2 ) and A7: dom g = cod f ; ::_thesis: g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] A8: ( dom g = k2 `11 & cod f = k1 `12 ) by A2, A3, A6; then A9: [k2,k1] in dom a9 by A4, A7; then A10: a9 . (k2,k1) = k2 * k1 by Def4; g (*) f = a9 . (g,f) by A6, A9, CAT_1:def_1; hence g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] by A1, A6, A7, A8, A10, Def3; ::_thesis: verum end; A11: for b being Element of CatStr(# O,M,D9,C9,a9 #) holds Hom (b,b) <> {} proof let b be Element of CatStr(# O,M,D9,C9,a9 #); ::_thesis: Hom (b,b) <> {} reconsider o = b as Element of commaObjs (F,G) ; set i = [[o,o],[(id (o `11)),(id (o `12))]]; reconsider g = id (o `11) as Morphism of C ; reconsider h = id (o `12) as Morphism of D ; A12: dom g = o `11 by CAT_1:58; A13: cod g = o `11 by CAT_1:58; A14: dom h = o `12 by CAT_1:58; A15: cod h = o `12 by CAT_1:58; o in commaObjs (F,G) ; then o in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } by A1, Def1; then consider c being Object of C, d being Object of D, f being Morphism of E such that A16: o = [[c,d],f] and A17: f in Hom ((F . c),(G . d)) ; A18: F . g = id (F . (o `11)) by CAT_1:71; A19: G . h = id (G . (o `12)) by CAT_1:71; A20: [[c,d],f] `2 = f ; A21: c = o `11 by A16, MCART_1:85; A22: d = o `12 by A16, MCART_1:85; A23: cod (o `2) = cod f by A20, A16 .= G . d by A17, CAT_1:1 .= G . (o `12) by A22 ; dom (o `2) = F . c by A16, A17, CAT_1:1, A20 .= F . (o `11) by A21 ; then A24: (o `2) (*) (F . g) = o `2 by A18, CAT_1:22 .= (G . h) (*) (o `2) by A19, A23, CAT_1:21 ; [[o,o],[(id (o `11)),(id (o `12))]] in { [[o1,o2],[gg,hh]] where gg is Morphism of C, hh is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom gg = o1 `11 & cod gg = o2 `11 & dom hh = o1 `12 & cod hh = o2 `12 & (o2 `2) (*) (F . gg) = (G . hh) (*) (o1 `2) ) } by A12, A13, A14, A15, A24; then [[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (F,G) by Def2, A1; then reconsider i = [[o,o],[(id (o `11)),(id (o `12))]] as Morphism of CatStr(# O,M,D9,C9,a9 #) ; A25: cod i = C9 . i .= [[o,o],[g,h]] `12 by A3 .= b by MCART_1:85 ; dom i = D9 . i .= [[o,o],[g,h]] `11 by A2 .= b by MCART_1:85 ; then i in Hom (b,b) by A25; hence Hom (b,b) <> {} ; ::_thesis: verum end; A26: for a being Element of CatStr(# O,M,D9,C9,a9 #) ex i being Morphism of a,a st for b being Element of CatStr(# O,M,D9,C9,a9 #) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) proof let a be Element of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ex i being Morphism of a,a st for b being Element of CatStr(# O,M,D9,C9,a9 #) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) reconsider o = a as Element of commaObjs (F,G) ; set i = [[o,o],[(id (o `11)),(id (o `12))]]; reconsider g = id (o `11) as Morphism of C ; reconsider h = id (o `12) as Morphism of D ; A27: dom g = o `11 by CAT_1:58; A28: cod g = o `11 by CAT_1:58; A29: dom h = o `12 by CAT_1:58; A30: cod h = o `12 by CAT_1:58; o in commaObjs (F,G) ; then o in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) } by A1, Def1; then consider c being Object of C, d being Object of D, f being Morphism of E such that A31: o = [[c,d],f] and A32: f in Hom ((F . c),(G . d)) ; A33: F . g = id (F . (o `11)) by CAT_1:71; A34: G . h = id (G . (o `12)) by CAT_1:71; A35: [[c,d],f] `2 = f ; A36: c = o `11 by A31, MCART_1:85; A37: d = o `12 by A31, MCART_1:85; A38: cod (o `2) = cod f by A35, A31 .= G . d by A32, CAT_1:1 .= G . (o `12) by A37 ; dom (o `2) = F . c by A31, A32, CAT_1:1, A35 .= F . (o `11) by A36 ; then A39: (o `2) (*) (F . g) = o `2 by A33, CAT_1:22 .= (G . h) (*) (o `2) by A34, A38, CAT_1:21 ; [[o,o],[(id (o `11)),(id (o `12))]] in { [[o1,o2],[gg,hh]] where gg is Morphism of C, hh is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom gg = o1 `11 & cod gg = o2 `11 & dom hh = o1 `12 & cod hh = o2 `12 & (o2 `2) (*) (F . gg) = (G . hh) (*) (o1 `2) ) } by A27, A28, A29, A30, A39; then [[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (F,G) by Def2, A1; then reconsider i = [[o,o],[(id (o `11)),(id (o `12))]] as Morphism of CatStr(# O,M,D9,C9,a9 #) ; A40: cod i = C9 . i .= [[o,o],[g,h]] `12 by A3 .= a by MCART_1:85 ; dom i = D9 . i .= [[o,o],[g,h]] `11 by A2 .= a by MCART_1:85 ; then i in Hom (a,a) by A40; then reconsider i = i as Morphism of a,a by CAT_1:def_5; take i ; ::_thesis: for b being Element of CatStr(# O,M,D9,C9,a9 #) holds ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) let b be Element of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) proof assume A41: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g let g be Morphism of a,b; ::_thesis: g (*) i = g reconsider gg = g as Element of commaMorphs (F,G) ; reconsider ii = i as Element of commaMorphs (F,G) ; A42: commaMorphs (F,G) = { [[o1,o2],[g1,h1]] where g1 is Morphism of C, h1 is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g1 = o1 `11 & cod g1 = o2 `11 & dom h1 = o1 `12 & cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) ) } by A1, Def2; gg in commaMorphs (F,G) ; then consider g1 being Morphism of C, h1 being Morphism of D, o1, o2 being Element of commaObjs (F,G) such that A43: gg = [[o1,o2],[g1,h1]] and A44: dom g1 = o1 `11 and cod g1 = o2 `11 and A45: dom h1 = o1 `12 and ( cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) ) by A42; A46: dom (commaComp (F,G)) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } by Def4; A47: ii `21 = [[o,o],[(id (o `11)),(id (o `12))]] `21 .= id (o `11) by MCART_1:85 ; A48: ii `22 = [[o,o],[(id (o `11)),(id (o `12))]] `22 .= id (o `12) by MCART_1:85 ; A49: o1 = [[o1,o2],[g1,h1]] `11 by MCART_1:85 .= gg `11 by A43 ; A50: o2 = [[o1,o2],[g1,h1]] `12 by MCART_1:85 .= gg `12 by A43 ; A51: g1 = [[o1,o2],[g1,h1]] `21 by MCART_1:85 .= gg `21 by A43 ; A52: h1 = [[o1,o2],[g1,h1]] `22 by MCART_1:85 .= gg `22 by A43 ; A53: dom g = a by A41, CAT_1:5; A54: dom g = gg `11 by A2 .= [[o1,o2],[g1,h1]] `11 by A43 .= o1 by MCART_1:85 ; A55: o1 = a by A41, CAT_1:5, A54 .= [[c,d],f] by A31 ; A56: dom (gg `21) = dom ([[o1,o2],[g1,h1]] `21) by A43 .= dom g1 by MCART_1:85 .= o1 `11 by A44 .= [[c,d],f] `11 by A55 .= o `11 by A31 ; A57: dom (gg `22) = dom ([[o1,o2],[g1,h1]] `22) by A43 .= dom h1 by MCART_1:85 .= o1 `12 by A45 .= [[c,d],f] `12 by A55 .= o `12 by A31 ; A58: ii `11 = [[o,o],[(id (o `11)),(id (o `12))]] `11 .= dom g by A53, MCART_1:85 .= D9 . gg .= gg `11 by A2 ; A59: ii `11 = o by MCART_1:85 .= ii `12 by MCART_1:85 ; then gg `11 = ii `12 by A58; then A60: [gg,ii] in dom (commaComp (F,G)) by A46; hence g (*) i = (commaComp (F,G)) . (g,i) by CAT_1:def_1 .= gg * ii by A60, Def4 .= [[(gg `11),(gg `12)],[((gg `21) (*) (id (o `11))),((gg `22) (*) (ii `22))]] by A1, A59, Def3, A58, A47 .= [[(gg `11),(gg `12)],[(gg `21),((gg `22) (*) (ii `22))]] by A56, CAT_1:22 .= [[(gg `11),(gg `12)],[(gg `21),(gg `22)]] by CAT_1:22, A48, A57 .= g by A49, A50, A51, A52, A43 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum proof assume A61: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f let g be Morphism of b,a; ::_thesis: i (*) g = g reconsider gg = g as Element of commaMorphs (F,G) ; reconsider ii = i as Element of commaMorphs (F,G) ; A62: commaMorphs (F,G) = { [[o1,o2],[g1,h1]] where g1 is Morphism of C, h1 is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g1 = o1 `11 & cod g1 = o2 `11 & dom h1 = o1 `12 & cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) ) } by A1, Def2; gg in commaMorphs (F,G) ; then consider g1 being Morphism of C, h1 being Morphism of D, o1, o2 being Element of commaObjs (F,G) such that A63: gg = [[o1,o2],[g1,h1]] and dom g1 = o1 `11 and A64: cod g1 = o2 `11 and dom h1 = o1 `12 and A65: cod h1 = o2 `12 and (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) by A62; A66: dom (commaComp (F,G)) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } by Def4; A67: ii `21 = [[o,o],[(id (o `11)),(id (o `12))]] `21 .= id (o `11) by MCART_1:85 ; A68: ii `22 = [[o,o],[(id (o `11)),(id (o `12))]] `22 .= id (o `12) by MCART_1:85 ; A69: o1 = [[o1,o2],[g1,h1]] `11 by MCART_1:85 .= gg `11 by A63 ; A70: o2 = [[o1,o2],[g1,h1]] `12 by MCART_1:85 .= gg `12 by A63 ; A71: g1 = [[o1,o2],[g1,h1]] `21 by MCART_1:85 .= gg `21 by A63 ; A72: h1 = [[o1,o2],[g1,h1]] `22 by MCART_1:85 .= gg `22 by A63 ; A73: cod g = a by A61, CAT_1:5; A74: cod g = gg `12 by A3 .= [[o1,o2],[g1,h1]] `12 by A63 .= o2 by MCART_1:85 ; A75: o2 = a by A61, CAT_1:5, A74 .= [[c,d],f] by A31 ; A76: cod (gg `21) = cod ([[o1,o2],[g1,h1]] `21) by A63 .= cod g1 by MCART_1:85 .= o2 `11 by A64 .= [[c,d],f] `11 by A75 .= o `11 by A31 ; A77: cod (gg `22) = cod ([[o1,o2],[g1,h1]] `22) by A63 .= cod h1 by MCART_1:85 .= o2 `12 by A65 .= [[c,d],f] `12 by A75 .= o `12 by A31 ; A78: ii `11 = [[o,o],[(id (o `11)),(id (o `12))]] `11 .= cod g by A73, MCART_1:85 .= C9 . gg .= gg `12 by A3 ; A79: ii `11 = o by MCART_1:85 .= ii `12 by MCART_1:85 ; gg `12 = ii `11 by A78; then A80: [ii,gg] in dom (commaComp (F,G)) by A66; hence i (*) g = (commaComp (F,G)) . (i,g) by CAT_1:def_1 .= ii * gg by A80, Def4 .= [[(gg `11),(gg `12)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]] by A1, A79, Def3, A78 .= [[(gg `11),(gg `12)],[(gg `21),((ii `22) (*) (gg `22))]] by A76, CAT_1:21, A67 .= [[(gg `11),(gg `12)],[(gg `21),(gg `22)]] by CAT_1:21, A68, A77 .= g by A69, A70, A71, A72, A63 ; ::_thesis: verum end; end; A81: for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) proof let f, g be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) assume A82: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) reconsider f1 = f, g1 = g as Element of commaMorphs (F,G) ; A83: ( dom g = g1 `11 & cod f = f1 `12 ) by A2, A3; then [g1,f1] in dom a9 by A4, A82; then A84: ( g (*) f = a9 . (g,f) & a9 . (g1,f1) = g1 * f1 ) by Def4, CAT_1:def_1; A85: ( dom f = f `11 & cod g = g `12 ) by A2, A3; A86: ( dom (g (*) f) = (g (*) f) `11 & cod (g (*) f) = (g (*) f) `12 ) by A2, A3; g1 * f1 = [[(f1 `11),(g1 `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]] by A1, A82, A83, Def3; hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A86, A85, A84, MCART_1:85; ::_thesis: verum end; A87: for f, g, h being Morphism of CatStr(# O,M,D9,C9,a9 #) st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f proof let f, g, h be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f ) reconsider f1 = f, g1 = g, h1 = h, gf = g (*) f, hg = h (*) g as Element of commaMorphs (F,G) ; assume that A88: dom h = cod g and A89: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f A90: ( dom g = g `11 & cod g = g `12 ) by A2, A3; dom (h (*) g) = dom g by A81, A88; then A91: (h (*) g) (*) f = [[(f `11),(hg `12)],[((hg `21) (*) (f1 `21)),((hg `22) (*) (f1 `22))]] by A5, A89; A92: ( dom h = h `11 & cod f = f `12 ) by A2, A3; cod (g (*) f) = cod g by A81, A89; then A93: h (*) (g (*) f) = [[(gf `11),(h `12)],[((h1 `21) (*) (gf `21)),((h1 `22) (*) (gf `22))]] by A5, A88; A94: ( dom (h1 `21) = (h1 `11) `11 & cod (f1 `21) = (f1 `12) `11 ) by A1, Th2; A95: ( dom (h1 `22) = (h1 `11) `12 & cod (f1 `22) = (f1 `12) `12 ) by A1, Th2; A96: ( dom (g1 `22) = (g1 `11) `12 & cod (g1 `22) = (g1 `12) `12 ) by A1, Th2; A97: h (*) g = [[(g `11),(h `12)],[((h1 `21) (*) (g1 `21)),((h1 `22) (*) (g1 `22))]] by A5, A88; then A98: ( (h (*) g) `12 = h `12 & hg `21 = (h1 `21) (*) (g1 `21) ) by MCART_1:85; A99: g (*) f = [[(f `11),(g `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]] by A5, A89; then A100: ( (g (*) f) `11 = f `11 & gf `21 = (g1 `21) (*) (f1 `21) ) by MCART_1:85; A101: gf `22 = (g1 `22) (*) (f1 `22) by A99, MCART_1:85; A102: hg `22 = (h1 `22) (*) (g1 `22) by A97, MCART_1:85; ( dom (g1 `21) = (g1 `11) `11 & cod (g1 `21) = (g1 `12) `11 ) by A1, Th2; then ((h1 `21) (*) (g1 `21)) (*) (f1 `21) = (h1 `21) (*) ((g1 `21) (*) (f1 `21)) by A88, A89, A90, A94, A92, CAT_1:18; hence h (*) (g (*) f) = (h (*) g) (*) f by A88, A89, A90, A92, A96, A95, A93, A91, A98, A100, A102, A101, CAT_1:18; ::_thesis: verum end; for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) holds ( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) iff dom g = cod f ) proof let f, g be Morphism of CatStr(# O,M,D9,C9,a9 #); ::_thesis: ( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) iff dom g = cod f ) reconsider f1 = f, g1 = g as Element of commaMorphs (F,G) ; A103: ( dom g = g1 `11 & cod f = f1 `12 ) by A2, A3; thus ( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) implies dom g = cod f ) ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) ) proof assume [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) ; ::_thesis: dom g = cod f then consider k1, k2 being Element of commaMorphs (F,G) such that A104: [g,f] = [k1,k2] and A105: k1 `11 = k2 `12 by A4; g = k1 by A104, XTUPLE_0:1; hence dom g = cod f by A103, A104, A105, XTUPLE_0:1; ::_thesis: verum end; thus ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) ) by A4, A103; ::_thesis: verum end; then reconsider FG = CatStr(# O,M,D9,C9,a9 #) as strict Category by A81, A87, A11, A26, CAT_1:def_6, CAT_1:def_7, CAT_1:def_8, CAT_1:def_9, CAT_1:def_10; take FG ; ::_thesis: ( the carrier of FG = commaObjs (F,G) & the carrier' of FG = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of FG . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of FG . k = k `12 ) & the Comp of FG = commaComp (F,G) ) thus ( the carrier of FG = commaObjs (F,G) & the carrier' of FG = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of FG . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of FG . k = k `12 ) & the Comp of FG = commaComp (F,G) ) by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being strict Category st the carrier of b1 = commaObjs (F,G) & the carrier' of b1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b1 . k = k `12 ) & the Comp of b1 = commaComp (F,G) & the carrier of b2 = commaObjs (F,G) & the carrier' of b2 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b2 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b2 . k = k `12 ) & the Comp of b2 = commaComp (F,G) holds b1 = b2 proof let E1, E2 be strict Category; ::_thesis: ( the carrier of E1 = commaObjs (F,G) & the carrier' of E1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of E1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of E1 . k = k `12 ) & the Comp of E1 = commaComp (F,G) & the carrier of E2 = commaObjs (F,G) & the carrier' of E2 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of E2 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of E2 . k = k `12 ) & the Comp of E2 = commaComp (F,G) implies E1 = E2 ) assume that A106: the carrier of E1 = commaObjs (F,G) and A107: the carrier' of E1 = commaMorphs (F,G) and A108: for k being Element of commaMorphs (F,G) holds the Source of E1 . k = k `11 and A109: for k being Element of commaMorphs (F,G) holds the Target of E1 . k = k `12 and A110: the Comp of E1 = commaComp (F,G) and A111: ( the carrier of E2 = commaObjs (F,G) & the carrier' of E2 = commaMorphs (F,G) ) and A112: for k being Element of commaMorphs (F,G) holds the Source of E2 . k = k `11 and A113: for k being Element of commaMorphs (F,G) holds the Target of E2 . k = k `12 and A114: the Comp of E2 = commaComp (F,G) ; ::_thesis: E1 = E2 now__::_thesis:_for_x_being_Element_of_H2(E1)_holds_the_Target_of_E1_._x_=_the_Target_of_E2_._x let x be Element of H2(E1); ::_thesis: the Target of E1 . x = the Target of E2 . x thus the Target of E1 . x = x `12 by A107, A109 .= the Target of E2 . x by A107, A113 ; ::_thesis: verum end; then A115: the Target of E1 = the Target of E2 by A106, A107, A111, FUNCT_2:63; now__::_thesis:_for_x_being_Element_of_H2(E1)_holds_the_Source_of_E1_._x_=_the_Source_of_E2_._x let x be Element of H2(E1); ::_thesis: the Source of E1 . x = the Source of E2 . x thus the Source of E1 . x = x `11 by A107, A108 .= the Source of E2 . x by A107, A112 ; ::_thesis: verum end; then the Source of E1 = the Source of E2 by A106, A107, A111, FUNCT_2:63; hence E1 = E2 by A106, A107, A110, A111, A114, A115; ::_thesis: verum end; end; :: deftheorem defines comma COMMACAT:def_5_:_ for C, D, E being Category for F being Functor of C,E for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds for b6 being strict Category holds ( b6 = F comma G iff ( the carrier of b6 = commaObjs (F,G) & the carrier' of b6 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b6 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b6 . k = k `12 ) & the Comp of b6 = commaComp (F,G) ) ); theorem :: COMMACAT:3 for y, x being set holds ( the carrier of (1Cat (x,y)) = {x} & the carrier' of (1Cat (x,y)) = {y} ) ; theorem Th4: :: COMMACAT:4 for y, x being set for a, b being Object of (1Cat (x,y)) holds Hom (a,b) = {y} proof let y, x be set ; ::_thesis: for a, b being Object of (1Cat (x,y)) holds Hom (a,b) = {y} let a, b be Object of (1Cat (x,y)); ::_thesis: Hom (a,b) = {y} thus Hom (a,b) c= {y} ; :: according to XBOOLE_0:def_10 ::_thesis: {y} c= Hom (a,b) y is Morphism of (1Cat (x,y)) by TARSKI:def_1; then y in Hom (a,b) by CAT_1:11; hence {y} c= Hom (a,b) by ZFMISC_1:31; ::_thesis: verum end; definition let C be Category; let c be Object of C; func 1Cat c -> strict Subcategory of C equals :: COMMACAT:def 6 1Cat (c,(id c)); coherence 1Cat (c,(id c)) is strict Subcategory of C proof A1: now__::_thesis:_for_a_being_Object_of_(1Cat_(c,(id_c))) for_c1_being_Object_of_C_st_a_=_c1_holds_ id_a_=_id_c1 let a be Object of (1Cat (c,(id c))); ::_thesis: for c1 being Object of C st a = c1 holds id a = id c1 id a = id c by TARSKI:def_1; hence for c1 being Object of C st a = c1 holds id a = id c1 by TARSKI:def_1; ::_thesis: verum end; A2: now__::_thesis:_for_a,_b_being_Object_of_(1Cat_(c,(id_c))) for_c1,_c2_being_Object_of_C_st_a_=_c1_&_b_=_c2_holds_ Hom_(a,b)_c=_Hom_(c1,c2) let a, b be Object of (1Cat (c,(id c))); ::_thesis: for c1, c2 being Object of C st a = c1 & b = c2 holds Hom (a,b) c= Hom (c1,c2) A3: ( a = c & b = c ) by TARSKI:def_1; ( id c in Hom (c,c) & Hom (a,a) = {(id c)} ) by Th4, CAT_1:27; hence for c1, c2 being Object of C st a = c1 & b = c2 holds Hom (a,b) c= Hom (c1,c2) by A3, ZFMISC_1:31; ::_thesis: verum end; set m = id c; set s = ((id c),(id c)) .--> (id c); A4: dom (((id c),(id c)) .--> (id c)) = {[(id c),(id c)]} by FUNCOP_1:13; A5: dom (id c) = c ; A6: cod (id c) = c ; A7: (((id c),(id c)) .--> (id c)) . ((id c),(id c)) = id c by FUNCOP_1:71; A8: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Comp_of_(1Cat_(c,(id_c)))_holds_ the_Comp_of_(1Cat_(c,(id_c)))_._x_=_the_Comp_of_C_._x let x be set ; ::_thesis: ( x in dom the Comp of (1Cat (c,(id c))) implies the Comp of (1Cat (c,(id c))) . x = the Comp of C . x ) assume A9: x in dom the Comp of (1Cat (c,(id c))) ; ::_thesis: the Comp of (1Cat (c,(id c))) . x = the Comp of C . x hence the Comp of (1Cat (c,(id c))) . x = id c by A7, A4, TARSKI:def_1 .= (id c) (*) (id c) by A6, CAT_1:21 .= the Comp of C . ((id c),(id c)) by A5, A6, CAT_1:16 .= the Comp of C . x by A4, A9, TARSKI:def_1 ; ::_thesis: verum end; [(id c),(id c)] in dom the Comp of C by A5, A6, CAT_1:15; then dom the Comp of (1Cat (c,(id c))) c= dom the Comp of C by A4, ZFMISC_1:31; then ( H1( 1Cat (c,(id c))) = {c} & the Comp of (1Cat (c,(id c))) c= the Comp of C ) by A8, GRFUNC_1:2; hence 1Cat (c,(id c)) is strict Subcategory of C by A2, A1, CAT_2:def_4; ::_thesis: verum end; end; :: deftheorem defines 1Cat COMMACAT:def_6_:_ for C being Category for c being Object of C holds 1Cat c = 1Cat (c,(id c)); definition let C be Category; let c be Object of C; funcc comma C -> strict Category equals :: COMMACAT:def 7 (incl (1Cat c)) comma (id C); coherence (incl (1Cat c)) comma (id C) is strict Category ; funcC comma c -> strict Category equals :: COMMACAT:def 8 (id C) comma (incl (1Cat c)); coherence (id C) comma (incl (1Cat c)) is strict Category ; end; :: deftheorem defines comma COMMACAT:def_7_:_ for C being Category for c being Object of C holds c comma C = (incl (1Cat c)) comma (id C); :: deftheorem defines comma COMMACAT:def_8_:_ for C being Category for c being Object of C holds C comma c = (id C) comma (incl (1Cat c));