Copyright (c) 1992 Association of Mizar Users
environ vocabulary CAT_1, MCART_1, FUNCT_1, RELAT_1, PARTFUN1, CAT_2, FUNCOP_1, FUNCT_3, COMMACAT; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, CAT_1, CAT_2, DOMAIN_1; constructors CAT_2, DOMAIN_1, MEMBERED, XBOOLE_0; clusters CAT_1, CAT_2, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; theorems TARSKI, ZFMISC_1, MCART_1, FUNCT_1, FUNCT_2, CAT_1, CAT_2, GRFUNC_1, RELSET_1; schemes FUNCT_2, ZFREFLE1; begin deffunc obj(CatStr) = the Objects of $1; deffunc morph(CatStr) = the Morphisms of $1; definition let x be set; func x`11 -> set equals: Def1: x`1`1; correctness; func x`12 -> set equals: Def2: x`1`2; correctness; func x`21 -> set equals: Def3: x`2`1; correctness; func x`22 -> set equals: Def4: x`2`2; correctness; end; reserve x,x1,x2,y,y1,y2,z for set; theorem Th1: [[x1,x2],y]`11 = x1 & [[x1,x2],y]`12 = x2 & [x,[y1,y2]]`21 = y1 & [x,[y1,y2]]`22 = y2 proof [[x1,x2],y]`1 = [x1,x2] & [x,[y1,y2]]`2 = [y1,y2] & [x1,x2]`1 = x1 & [y1,y2]`1 = y1 & [x1,x2]`2 = x2 & [y1,y2]`2 = y2 by MCART_1:7; hence thesis by Def1,Def2,Def3,Def4; end; definition let D1,D2,D3 be non empty set, x be Element of [:[:D1,D2:],D3:]; redefine func x`11 -> Element of D1; coherence proof x`11 = x`1`1 by Def1; hence thesis; end; func x`12 -> Element of D2; coherence proof x`12 = x`1`2 by Def2; hence thesis; end; end; definition let D1,D2,D3 be non empty set, x be Element of [:D1,[:D2,D3:]:]; redefine func x`21 -> Element of D2; coherence proof x`21 = x`2`1 by Def3; hence thesis; end; func x`22 -> Element of D3; coherence proof x`22 = x`2`2 by Def4; hence thesis; end; end; reserve C,D,E for Category, c,c1,c2 for Object of C, d,d1 for Object of D, x for set, f,f1 for (Morphism of E), g for (Morphism of C), h for (Morphism of D), F for Functor of C,E, G for Functor of D,E; definition let C,D,E; let F be Functor of C,E, G be Functor of D,E; given c1,d1,f1 such that A1: f1 in Hom(F.c1,G.d1); func commaObjs(F,G) -> non empty Subset of [:[:the Objects of C, the Objects of D:], the Morphisms of E:] equals: Def5: {[[c,d],f] : f in Hom(F.c,G.d)}; coherence proof A2: [[c1,d1],f1] in {[[c,d],f] : f in Hom(F.c,G.d)} by A1; {[[c,d],f] : f in Hom(F.c,G.d)} c= [:[:the Objects of C, the Objects of D:], the Morphisms of E:] proof let x; assume x in {[[c,d],f] : f in Hom(F.c,G.d)}; then ex c,d,f st x = [[c,d],f] & f in Hom(F.c,G.d); hence thesis; end; hence thesis by A2; end; end; reserve o,o1,o2 for Element of commaObjs(F,G); theorem Th2: (ex c,d,f 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 proof assume ex c,d,f st f in Hom(F.c,G.d); then o in commaObjs(F,G) & commaObjs(F,G) = {[[c,d],f]: f in Hom(F.c,G.d)} by Def5; then consider c,d,f such that A1: o = [[c,d],f] & f in Hom(F.c,G.d); o`11 = c & o`12 = d & o`2 = f by A1,Th1,MCART_1:7; hence thesis by A1,CAT_1:18; end; definition let C,D,E,F,G; given c1,d1,f1 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 Morphisms of C, the Morphisms of D:]:] equals: Def6: {[[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)}; coherence proof set 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)}; commaObjs(F,G) = {[[c,d],f] : f in Hom(F.c,G.d)} by A1,Def5; then [[c1,d1],f1] in commaObjs(F,G) by A1; then reconsider o = [[c1,d1],f1] as Element of commaObjs(F,G); dom f1 = F.c1 & cod f1 = G.d1 by A1,CAT_1:18; then dom id c1 = c1 & cod id c1 = c1 & dom id d1 = d1 & cod id d1 = d1 & o`1`1 = o`11 & o`1`2 = o`12 & o`1 = [c1,d1] & [c1,d1]`1 = c1 & [c1,d1]`2 = d1 & o`2 = f1 & f1*id(F.c1) = f1 & id(G.d1)*f1 = f1 & F.id c1 = id(F.c1) & G.id d1 = id(G.d1) by Def1,Def2,CAT_1:44,46,47,108,MCART_1:7; then A2: [[o,o],[id c1,id d1]] in X; X c= [:[:commaObjs(F,G), commaObjs(F,G):], [:the Morphisms of C, the Morphisms of D:]:] proof let x; assume x in X; then ex g,h,o1,o2 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 thesis; end; hence thesis by A2; end; end; reserve k,k1,k2,k' for Element of commaMorphs(F,G); definition let C,D,E,F,G,k; redefine func k`11 -> Element of commaObjs(F,G); coherence proof thus k`11 is Element of commaObjs(F,G); end; func k`12 -> Element of commaObjs(F,G); coherence proof thus k`12 is Element of commaObjs(F,G); end; end; theorem Th3: (ex c,d,f 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) proof assume ex c,d,f st f in Hom(F.c,G.d); then commaMorphs(F,G) = {[[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)} & k in commaMorphs(F,G) by Def6; then consider g,h,o1,o2 such that A1: k = [[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); k`11 = o1 & k`12 = o2 & k`21 = g & k`22 = h by A1,Th1; hence thesis by A1; end; definition let C,D,E,F,G,k1,k2; given c1,d1,f1 such that A1: f1 in Hom(F.c1,G.d1); assume A2: k1`12 = k2`11; func k2*k1 -> Element of commaMorphs(F,G) equals: Def7: [[k1`11,k2`12],[k2`21*k1`21,k2`22*k1`22]]; coherence proof set k21 = k2`21*k1`21; set k22 = k2`22*k1`22; A3: dom k1`21 = k1`11`11 & cod k1`21 = k1`12`11 & dom k1`22 = k1`11`12 & cod k1`22 = k1`12`12 & (k1`12`2)*(F.k1`21) = (G.k1`22)*(k1`11`2) by A1,Th3; A4: dom k2`21 = k2`11`11 & cod k2`21 = k2`12`11 & dom k2`22 = k2`11`12 & cod k2`22 = k2`12`12 & (k2`12`2)*(F.k2`21) = (G.k2`22)*(k2`11`2) by A1,Th3; A5: dom k1`11`2 = F.k1`11`11 & cod k1`11`2 = G.k1`11`12 & dom k1`12`2 = F.k1`12`11 & cod k1`12`2 = G.k1`12`12 & dom k2`11`2 = F.k2`11`11 & cod k2`11`2 = G.k2`11`12 & dom k2`12`2 = F.k2`12`11 & cod k2`12`2 = G.k2`12`12 by A1,Th2; A6: F.cod k2`21 = cod (F.k2`21) & dom (F.k2`21) = F.dom k2`21 & cod (F.k1`21) = F.cod k1`21 & dom (G.k2`22) = G.dom k2`22 & dom (G.k1`22) = G.dom k1`22 & cod (G.k1`22) = G.cod k1`22 by CAT_1:109; A7: commaMorphs(F,G) = {[[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)} by A1,Def6; A8: dom k21 = dom k1`21 & cod k21 = cod k2`21 & dom k22 = dom k1`22 & cod k22 = cod k2`22 by A2,A3,A4,CAT_1:42; ((k2`12)`2)*(F.k21) = (k2`12`2)*((F.k2`21)*(F.k1`21)) by A2,A3,A4,CAT_1:99 .= (G.k2`22)*(k2`11`2)*(F.k1`21) by A2,A3,A4,A5,A6,CAT_1:43 .= (G.k2`22)*((G.k1`22)*(k1`11`2)) by A2,A3,A4,A5,A6,CAT_1:43 .= (G.k2`22)*(G.k1`22)*(k1`11`2) by A2,A3,A4,A5,A6,CAT_1:43 .= (G.k22)*((k1`11)`2) by A2,A3,A4,CAT_1:99; then ([[k1`11,k2`12],[k2`21*k1`21,k2`22*k1`22]]) in commaMorphs(F,G) by A3,A4,A7,A8; hence thesis; end; end; definition let C,D,E,F,G; func commaComp(F,G) -> PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):],commaMorphs(F,G) means: Def8: dom it = { [k1,k2]: k1`11 = k2`12 } & for k,k' st [k,k'] in dom it holds it.[k,k'] = k*k'; existence proof set X = {[k1,k2]: k1`11 = k2`12}; defpred P[set,set] means ex k1,k2 st $1 = [k1,k2] & $2 = k1*k2; A1: for x st x in X ex y st P[x,y] proof let x; assume x in X; then consider k1,k2 such that A2: x = [k1,k2] & k1`11 = k2`12; reconsider y = k1*k2 as set; take y,k1,k2; thus thesis by A2; end; consider f being Function such that A3: dom f = X & for x st x in X holds P[x,f.x] from NonUniqFuncEx(A1); A4: dom f c= [:commaMorphs(F,G),commaMorphs(F,G):] proof let x; assume x in dom f; then ex k1,k2 st x = [k1,k2] & k1`11 = k2`12 by A3; hence x in [:commaMorphs(F,G),commaMorphs(F,G):]; end; rng f c= commaMorphs(F,G) proof let x; assume x in rng f; then consider y such that A5: y in dom f & x = f.y by FUNCT_1:def 5; ex k1,k2 st y = [k1,k2] & f.y = k1*k2 by A3,A5; hence thesis by A5; end; then reconsider f as PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):], commaMorphs(F,G) by A4,RELSET_1:11; take f; thus dom f = X by A3; let k1,k2; assume [k1,k2] in dom f; then consider k,k' such that A6: [k1,k2] = [k,k'] & f.[k1,k2] = k*k' by A3; k1 = k & k2 = k' by A6,ZFMISC_1:33; hence thesis by A6; end; uniqueness proof let f1,f2 be PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):], commaMorphs(F,G) such that A7: dom f1 = { [k1,k2]: k1`11 = k2`12 } & for k,k' st [k,k'] in dom f1 holds f1.[k,k'] = k*k' and A8: dom f2 = { [k1,k2]: k1`11 = k2`12 } & for k,k' st [k,k'] in dom f2 holds f2.[k,k'] = k*k'; now let x; assume A9: x in { [k1,k2]: k1`11 = k2`12 }; then consider k1,k2 such that A10: x = [k1,k2] & k1`11 = k2`12; thus f1.x = k1*k2 by A7,A9,A10 .= f2.x by A8,A9,A10; end; hence thesis by A7,A8,FUNCT_1:9; end; end; definition let C,D,E,F,G; given c1,d1,f1 such that A1: f1 in Hom(F.c1,G.d1); func F comma G -> strict Category means the Objects of it = commaObjs(F,G) & the Morphisms of it = commaMorphs(F,G) & (for k holds (the Dom of it).k = k`11) & (for k holds (the Cod of it).k = k`12) & (for o holds (the Id of it).o = [[o,o], [id o`11,id o`12]]) & the Comp of it = commaComp(F,G); existence proof deffunc F(Element of commaMorphs(F,G)) = $1`11; deffunc G(Element of commaMorphs(F,G)) = $1`12; consider D' being Function of commaMorphs(F,G),commaObjs(F,G) such that A2: D'.k = F(k) from LambdaD; consider C' being Function of commaMorphs(F,G),commaObjs(F,G) such that A3: C'.k = G(k) from LambdaD; A4: commaObjs(F,G) = {[[c,d],f] : f in Hom(F.c,G.d)} & commaMorphs(F,G) = {[[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)} by A1,Def5,Def6; defpred P[ Element of commaObjs(F,G),set] means $2 = [[$1,$1],[id $1`11, id $1`12]]; A5: ex k st P[o,k] proof A6: dom o`2 = F.o`11 & cod o`2 = G.o`12 & dom id o`11 = o`11 & cod id o`11 = o`11 & dom id o`12 = o`12 & cod id o`12 = o`12 & F.id o`11 = id (F.o`11) & G.id o`12 = id (G.o`12) by A1,Th2,CAT_1:44,108; then o`2*(F.id o`11) = o`2 & (G.id o`12)*o`2 = o`2 by CAT_1:46,47; then [[o,o],[id o`11,id o`12]] in commaMorphs(F,G) by A4,A6; hence thesis; end; consider I being Function of commaObjs(F,G),commaMorphs(F,G) such that A7: P[o,I.o] from FuncExD(A5); reconsider O = commaObjs(F,G), M = commaMorphs(F,G) as non empty set; reconsider D', C' as Function of M,O; reconsider ' = commaComp(F,G) as PartFunc of [:M,M:],M; reconsider I as Function of O,M; set FG = CatStr(#O, M, D', C', ', I#); A8: dom the Comp of FG = { [k1,k2]: k1`11 = k2`12} by Def8; A9: for f being Morphism of FG holds dom f = f`11 & cod f = f`12 proof let f be Morphism of FG; dom f = D'.f & cod f = C'.f by CAT_1:def 2,def 3; hence thesis by A2,A3; end; A10: for f,g being Morphism of FG for k1,k2 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 FG; let k1,k2; assume A11: f = k1 & g = k2 & dom g = cod f; then A12: dom g = k2`11 & cod f = k1`12 by A9; then [k2,k1] in dom ' by A8,A11; then g*f = '.[g,f] & '.[k2,k1] = k2*k1 & k2*k1 = [[k1`11,k2`12],[k2`21*k1`21,k2`22*k1`22]] by A1,A11,A12,Def7,Def8,CAT_1:def 4; hence thesis by A11; end; A13: for f,g being Morphism of FG holds [g,f] in dom the Comp of FG iff dom g = cod f proof let f,g be Morphism of FG; reconsider f1 = f, g1 = g as Element of commaMorphs(F,G); A14: dom g = g1`11 & cod f = f1`12 by A9; thus [g,f] in dom the Comp of FG implies dom g = cod f proof assume [g,f] in dom the Comp of FG; then consider k1,k2 such that A15: [g,f] = [k1,k2] & k1`11 = k2`12 by A8; g = k1 & f = k2 by A15,ZFMISC_1:33; hence thesis by A14,A15; end; thus thesis by A8,A14; end; A16: for f,g being Morphism of FG st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g proof let f,g be Morphism of FG such that A17: dom g = cod f; reconsider f1 = f, g1 = g as Element of commaMorphs(F,G); A18: dom g = g1`11 & cod f = f1`12 & dom (g*f) = (g*f)`11 & cod (g*f) = (g*f)`12 & dom f = f`11 & cod g = g`12 by A9; then [g1,f1] in dom ' by A8,A17; then g*f = '.[g,f] & '.[g1,f1] = g1*f1 & g1*f1 = [[f1`11,g1`12],[g1`21*f1`21,g1`22*f1`22]] by A1,A17,A18,Def7,Def8,CAT_1:def 4; hence thesis by A18,Th1; end; A19: for f,g,h being Morphism of FG st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f proof let f,g,h be Morphism of FG; reconsider f1 = f, g1 = g, h1 = h, gf = g*f, hg = h*g as Element of commaMorphs(F,G); assume A20: dom h = cod g & dom g = cod f; then g*f = [[f`11,g`12],[g1`21*f1`21,g1`22*f1`22]] & dom g = g`11 & h*g = [[g`11,h`12],[h1`21*g1`21,h1`22*g1`22]] & cod g = g`12 & dom g1`21 = g1`11`11 & cod g1`21 = g1`12`11 & dom h = h`11 & dom h1`21 = h1`11`11 & cod f1`21 = f1`12`11 & cod f = f`12 & dom g1`22 = g1`11`12 & cod g1`22 = g1`12`12 & dom h1`22 = h1`11`12 & cod f1`22 = f1`12`12 & cod (g*f) = cod g & dom (h*g) = dom g by A1,A9,A10,A16,Th3; then h*(g*f) = [[gf`11,h`12],[h1`21*gf`21,h1`22*gf`22]] & (h*g)*f = [[f`11,hg`12],[hg`21*f1`21,hg`22*f1`22]] & (g*f)`11 = f`11 & (h*g)`12 = h`12 & hg`21 = h1`21*g1`21 & gf`21 = g1`21*f1`21 & hg`22 = h1`22*g1`22 & gf`22 = g1`22*f1`22 & (h1`21*g1`21)*f1`21 = h1`21*(g1`21*f1`21) & (h1`22*g1`22)*f1`22 = h1`22*(g1`22*f1`22) by A10,A20,Th1,CAT_1:43; hence thesis; end; for b being Object of FG holds dom id b = b & cod id b = b & (for f being Morphism of FG st cod f = b holds (id b)*f = f) & (for g being Morphism of FG st dom g = b holds g*(id b) = g) proof let b be Object of FG; reconsider b' = b as Element of commaObjs(F,G); reconsider i = id b as Element of commaMorphs(F,G); I.b' = [[b',b'],[id b'`11, id b'`12]] by A7; then A21: (I.b')`11 = b' & (I.b')`12 = b' & (I.b')`21 = id b'`11 & (I.b')`22 = id b'`12 & i = I.b by Th1,CAT_1:def 5; hence dom id b = b & cod id b = b by A9; thus for f being Morphism of FG st cod f = b holds (id b)*f = f proof let f be Morphism of FG; reconsider f' = f as Element of commaMorphs(F,G); assume cod f = b; then A22: cod f = dom id b & dom id b'`12 = b'`12 & dom id b'`11 = b' `11 & b = f`12 & cod f'`21 = f'`12`11 & cod f'`22 = f'`12`12 by A1,A9,A21,Th3; then A23: (id b'`11)*f'`21 = f'`21 & (id b'`12)*f'`22 = f'`22 by CAT_1: 46; thus (id b)*f = [[f'`11,i`12],[i`21*f'`21,i`22*f'`22]] by A10,A22 .= f by A1,A21,A22,A23,Th3; end; let g be Morphism of FG; reconsider g' = g as Element of commaMorphs(F,G); assume dom g = b; then A24: dom g = cod id b & dom id b'`12 = b'`12 & dom id b'`11 = b'`11 & b = g`11 & dom g'`21 = g'`11`11 & dom g'`22 = g'`11`12 by A1,A9,A21,Th3; then A25: g'`21*(id b'`11) = g'`21 & g'`22*(id b'`12) = g'`22 by CAT_1:47; thus g*(id b) = [[i`11,g'`12],[g'`21*i`21,g'`22*i`22]] by A10,A24 .= g by A1,A21,A24,A25,Th3; end; then reconsider FG as strict Category by A13,A16,A19,CAT_1:29; take FG; thus thesis by A2,A3,A7; end; uniqueness proof let E1,E2 be strict Category such that A26: the Objects of E1 = commaObjs(F,G) & the Morphisms of E1 = commaMorphs(F,G) & (for k holds (the Dom of E1).k = k`11) & (for k holds (the Cod of E1).k = k`12) & (for o holds (the Id of E1).o = [[o,o], [id o`11,id o`12]]) & the Comp of E1 = commaComp(F,G) and A27: the Objects of E2 = commaObjs(F,G) & the Morphisms of E2 = commaMorphs(F,G) & (for k holds (the Dom of E2).k = k`11) & (for k holds (the Cod of E2).k = k`12) & (for o holds (the Id of E2).o = [[o,o], [id o`11,id o`12]]) & the Comp of E2 = commaComp(F,G); now let x be Element of morph(E1); thus (the Dom of E1).x = x`11 by A26 .= (the Dom of E2).x by A26,A27; end; then A28: the Dom of E1 = the Dom of E2 by A26,A27,FUNCT_2:113; now let x be Element of morph(E1); thus (the Cod of E1).x = x`12 by A26 .= (the Cod of E2).x by A26,A27; end; then A29: the Cod of E1 = the Cod of E2 by A26,A27,FUNCT_2:113; now let x be Object of E1; reconsider o = x as Element of commaObjs(F,G) by A26; thus (the Id of E1).x = [[o,o],[id o`11,id o`12]] by A26 .= (the Id of E2).x by A27; end; hence thesis by A26,A27,A28,A29,FUNCT_2:113; end; end; theorem Th4: the Objects of 1Cat(x,y) = {x} & the Morphisms of 1Cat(x,y) = {y} proof thus obj(1Cat(x,y)) c= {x} proof let z; assume z in obj(1Cat(x,y)); then z = x by CAT_1:34; hence thesis by TARSKI:def 1; end; x is Object of 1Cat(x,y) by CAT_1:32; hence {x} c= obj(1Cat(x,y)) by ZFMISC_1:37; thus morph(1Cat(x,y)) c= {y} proof let z; assume z in morph(1Cat(x,y)); then z = y by CAT_1:35; hence thesis by TARSKI:def 1; end; y is Morphism of 1Cat(x,y) by CAT_1:33; hence {y} c= morph(1Cat(x,y)) by ZFMISC_1:37; end; theorem Th5: for a,b being Object of 1Cat(x,y) holds Hom(a,b) = {y} proof let a,b be Object of 1Cat(x,y); morph(1Cat(x,y)) = {y} by Th4; hence Hom(a,b) c= {y}; y is Morphism of 1Cat(x,y) by CAT_1:33; then y in Hom(a,b) by CAT_1:36; hence thesis by ZFMISC_1:37; end; definition let C, c; func 1Cat c -> strict Subcategory of C equals 1Cat(c, id c); coherence proof A1: obj(1Cat(c, id c)) = {c} by Th4; A2: now let a,b be Object of 1Cat(c, id c); a = c & b = c & id c in Hom(c,c) & Hom(a,a) = {id c} by Th5,CAT_1:34,55; hence for c1,c2 st a = c1 & b = c2 holds Hom(a,b) c= Hom(c1,c2) by ZFMISC_1:37; end; set m = id c; reconsider O = {c}, M = {id c} as non empty set; reconsider d = M-->c as Function of M,O; reconsider i = O-->m as Function of O,M; reconsider s = (m,m).--> m as PartFunc of [:M,M:],M; A3: 1Cat(c,m) = CatStr(#O, M, d, d, s, i#) & dom s = {[m,m]} & s.[m,m] = m by CAT_1:7,8,def 9; A4: dom m = c & cod m = c by CAT_1:44; then [m,m] in dom the Comp of C by CAT_1:40; then A5: dom the Comp of 1Cat(c,m) c= dom the Comp of C by A3,ZFMISC_1:37; now let x; assume A6: x in dom the Comp of 1Cat(c,m); then A7: x = [m,m] by A3,TARSKI:def 1; thus (the Comp of 1Cat(c,m)).x = m by A3,A6,TARSKI:def 1 .= m*(m qua Morphism of C) by A4,CAT_1:46 .= (the Comp of C).x by A4,A7,CAT_1:41; end; then A8: the Comp of 1Cat(c, id c) <= the Comp of C by A5,GRFUNC_1:8; now let a be Object of 1Cat(c, id c); id a = id c & a = c by CAT_1:34,35; hence for c1 st a = c1 holds id a = id c1; end; hence thesis by A1,A2,A8,CAT_2:def 4; end; correctness; end; definition let C, c; func c comma C -> strict Category equals (incl 1Cat c) comma (id C); correctness; func C comma c -> strict Category equals (id C) comma (incl 1Cat c); correctness; end;