Copyright (c) 1989 Association of Mizar Users
environ vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCOP_1, PARTFUN1, TARSKI, WELLORD1, CAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1; constructors FUNCOP_1, WELLORD2, MEMBERED, PARTFUN1, XBOOLE_0; clusters FUNCT_1, RELSET_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI; theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, PARTFUN1, FUNCOP_1, SUBSET_1, WELLORD2, RELAT_1, RELSET_1, XBOOLE_1; schemes FUNCT_2; begin :: Auxiliary theorems reserve a,b,c,o,m for set; canceled 3; theorem Th4: for X,Y,Z being set, D being non empty set, f being Function of X,D st Y c= X & f.:Y c= Z holds f|Y is Function of Y,Z proof let X,Y,Z be set, D be non empty set, f be Function of X,D; assume that A1: Y c= X and A2: f.:Y c= Z; dom f = X by FUNCT_2:def 1; then A3: dom(f|Y) = Y by A1,RELAT_1:91; A4: rng(f|Y) c= Z by A2,RELAT_1:148; now assume Z = {}; then rng(f|Y) = {} by A4,XBOOLE_1:3; hence Y = {} by A3,RELAT_1:65; end; hence f|Y is Function of Y,Z by A3,A4,FUNCT_2:def 1,RELSET_1:11; end; definition let A be non empty set,b; redefine func A --> b -> Function of A,{b}; coherence proof {b} <> {} & dom(A --> b) = A & rng(A --> b) c= {b} by FUNCOP_1:19; hence thesis by FUNCT_2:def 1,RELSET_1:11; end; end; definition let a,b,c; func (a,b).-->c -> PartFunc of [:{a},{b}:],{c} equals :Def1: {[a,b]} --> c; correctness proof [:{a},{b}:] = {[a,b]} by ZFMISC_1:35; hence thesis; end; end; canceled 2; theorem Th7: dom (a,b).-->c = {[a,b]} & dom (a,b).-->c = [:{a},{b}:] proof (a,b).-->c = {[a,b]} --> c by Def1; hence dom (a,b).-->c = {[a,b]} by FUNCT_2:def 1; hence dom (a,b).-->c = [:{a},{b}:] by ZFMISC_1:35; end; theorem Th8: ((a,b).-->c).[a,b] = c proof [:{a},{b}:] = {[a,b]} & [a,b] in {[a,b]} & (a,b).-->c = {[a,b]} --> c by Def1,TARSKI:def 1,ZFMISC_1:35; hence thesis by FUNCT_2:65; end; theorem Th9: for x being Element of {a} for y being Element of {b} holds ((a,b).-->c).[x,y] = c proof let x be Element of {a}; let y be Element of {b}; x = a & y = b by TARSKI:def 1; hence thesis by Th8; end; :: Structure of a Category definition struct CatStr (# Objects,Morphisms -> non empty set, Dom,Cod -> Function of the Morphisms, the Objects, Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms, Id -> Function of the Objects, the Morphisms #); end; reserve C for CatStr; definition let C; mode Object of C is Element of the Objects of C; mode Morphism of C is Element of the Morphisms of C; end; reserve a,b,c,d for Object of C; reserve f,g for Morphism of C; :: Domain and Codomain of a Morphism definition let C,f; func dom(f) -> Object of C equals :Def2: (the Dom of C).f; correctness; func cod(f) -> Object of C equals :Def3: (the Cod of C).f; correctness; end; definition let C,f,g; assume A1: [g,f] in dom(the Comp of C); func g*f -> Morphism of C equals :Def4: ( the Comp of C ).[g,f]; coherence by A1,PARTFUN1:27; end; definition let C,a; func id (a) -> Morphism of C equals :Def5: ( the Id of C ).a; correctness; end; definition let C,a,b; func Hom(a,b) -> Subset of the Morphisms of C equals :Def6: { f : dom(f)=a & cod(f)=b }; correctness proof set M = { f : dom(f)=a & cod(f)=b }; M c= the Morphisms of C proof let x be set; assume x in M; then ex f st x = f & dom(f)=a & cod(f)=b; hence thesis; end; hence thesis; end; end; canceled 8; theorem Th18: f in Hom(a,b) iff dom(f)=a & cod(f)=b proof A1: Hom(a,b) = { g : dom(g)=a & cod(g)=b } by Def6; thus f in Hom(a,b) implies dom(f) = a & cod(f) = b proof assume f in Hom(a,b); then ex g st f = g & dom(g) = a & cod(g) = b by A1; hence thesis; end; thus thesis by A1; end; theorem Hom(dom(f),cod(f)) <> {} by Th18; definition let C,a,b; assume A1: Hom(a,b)<>{}; mode Morphism of a,b -> Morphism of C means :Def7: it in Hom(a,b); existence by A1,SUBSET_1:10; end; canceled; theorem for f being set st f in Hom(a,b) holds f is Morphism of a,b by Def7; theorem Th22: for f being Morphism of C holds f is Morphism of dom(f),cod(f) proof let f be Morphism of C; f in Hom(dom(f),cod(f)) by Th18; hence f is Morphism of dom(f),cod(f) by Def7; end; theorem Th23: for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b proof let f be Morphism of a,b; assume Hom(a,b) <> {}; then f in Hom(a,b) by Def7; hence dom(f) = a & cod(f) = b by Th18; end; theorem for f being Morphism of a,b for h being Morphism of c,d st Hom(a,b) <> {} & Hom(c,d) <> {} & f = h holds a = c & b = d proof let f be Morphism of a,b; let h be Morphism of c,d; assume Hom(a,b) <> {} & Hom(c,d) <> {}; then dom(f) = a & cod(f) = b & dom(h) = c & cod(h) = d by Th23; hence thesis; end; theorem Th25: for f being Morphism of a,b st Hom(a,b) = {f} for g being Morphism of a,b holds f = g proof let f be Morphism of a,b such that A1: Hom(a,b) = {f}; let g be Morphism of a,b; g in {f} by A1,Def7; hence thesis by TARSKI:def 1; end; theorem Th26: for f being Morphism of a,b st Hom(a,b) <> {} & for g being Morphism of a,b holds f = g holds Hom(a,b) = {f} proof let f be Morphism of a,b such that A1: Hom(a,b) <> {} and A2: for g being Morphism of a,b holds f = g; for x being set holds x in Hom(a,b) iff x = f proof let x be set; thus x in Hom(a,b) implies x = f proof A3: Hom(a,b) = { g: dom(g)=a & cod(g)=b } by Def6; assume x in Hom(a,b); then consider g being Morphism of C such that A4: x = g and A5: dom(g)=a & cod(g)=b by A3; g is Morphism of a,b by A5,Th22; hence thesis by A2,A4; end; thus thesis by A1,Def7; end; hence thesis by TARSKI:def 1; end; theorem for f being Morphism of a,b st Hom(a,b),Hom(c,d) are_equipotent & Hom(a,b) = {f} holds ex h being Morphism of c,d st Hom(c,d) = {h} proof let f be Morphism of a,b; assume Hom(a,b),Hom(c,d) are_equipotent; then consider F being Function such that F is one-to-one and A1: dom F = Hom(a,b) & rng F = Hom(c,d) by WELLORD2:def 4; assume Hom(a,b) = {f}; then A2: Hom(c,d) = {F.f} by A1,FUNCT_1:14; then F.f in Hom(c,d) by TARSKI:def 1; then F.f is Morphism of c,d by Def7; hence thesis by A2; end; Lm1: now let o,m be set; let C be CatStr such that A1: C = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #); set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C, CI = the Id of C; thus for f,g being Element of the Morphisms of C holds [g,f] in dom CP iff CD.g=CC.f proof let f,g be Element of the Morphisms of C; f = m & g = m & dom CP = {[m,m]} by A1,Th7,TARSKI:def 1; hence thesis by A1,TARSKI:def 1; end; thus for f,g being Element of the Morphisms of C st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g proof let f,g be Element of the Morphisms of C; CP.[g,f] = m by A1,Th9; then reconsider gf = CP.[g,f] as Element of the Morphisms of C by A1, TARSKI:def 1; CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65; hence thesis; end; thus for f,g,h being Element of the Morphisms of C st CD.h = CC.g & CD.g = CC.f holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f] proof let f,g,h be Element of the Morphisms of C; CP.[g,f] = m & CP.[h,g] = m by A1,Th9; then reconsider gf = CP.[g,f],hg = CP.[h,g] as Element of the Morphisms of C by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,Th9; hence thesis; end; let b be Element of the Objects of C; b = o by A1,TARSKI:def 1; hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65; thus for f being Element of the Morphisms of C st CC.f = b holds CP.[CI.b,f] = f proof let f be Element of the Morphisms of C; f = m by A1,TARSKI:def 1; hence thesis by A1,Th9; end; let g be Element of the Morphisms of C; g = m by A1,TARSKI:def 1; hence CP.[g,CI.b] = g by A1,Th9; end; :: Category definition let C be CatStr; attr C is Category-like means :Def8: (for f,g being Element of the Morphisms of C holds [g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f) & (for f,g being Element of the Morphisms of C st (the Dom of C).g=(the Cod of C).f holds (the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f & (the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g) & (for f,g,h being Element of the Morphisms of C st (the Dom of C).h = (the Cod of C).g & (the Dom of C).g = (the Cod of C).f holds (the Comp of C).[h,(the Comp of C).[g,f]] = (the Comp of C).[(the Comp of C).[h,g],f] ) & (for b being Element of the Objects of C holds (the Dom of C).((the Id of C).b) = b & (the Cod of C).((the Id of C).b) = b & (for f being Element of the Morphisms of C st (the Cod of C).f = b holds (the Comp of C).[(the Id of C).b,f] = f ) & (for g being Element of the Morphisms of C st (the Dom of C).g = b holds (the Comp of C).[g,(the Id of C).b] = g ) ); end; definition cluster Category-like CatStr; existence proof take C = CatStr(# {0},{1},{1}-->0,{1}-->0,(1,1).-->1,{0}-->1 #); thus (for f,g being Element of the Morphisms of C holds [g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f) & (for f,g being Element of the Morphisms of C st (the Dom of C).g=(the Cod of C).f holds (the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f & (the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g) & (for f,g,h being Element of the Morphisms of C st (the Dom of C).h = (the Cod of C).g & (the Dom of C).g = (the Cod of C).f holds (the Comp of C).[h,(the Comp of C).[g,f]] = (the Comp of C).[(the Comp of C).[h,g],f] ) & (for b being Element of the Objects of C holds (the Dom of C).((the Id of C).b) = b & (the Cod of C).((the Id of C).b) = b & (for f being Element of the Morphisms of C st (the Cod of C).f = b holds (the Comp of C).[(the Id of C).b,f] = f ) & (for g being Element of the Morphisms of C st (the Dom of C).g = b holds (the Comp of C).[g,(the Id of C).b] = g ) ) by Lm1; end; end; definition mode Category is Category-like CatStr; end; definition cluster strict Category; existence proof set C = CatStr(# {0},{1},{1}-->0,{1}-->0,(1,1).-->1,{0}-->1 #); (for f,g being Element of the Morphisms of C holds [g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f) & (for f,g being Element of the Morphisms of C st (the Dom of C).g=(the Cod of C).f holds (the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f & (the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g) & (for f,g,h being Element of the Morphisms of C st (the Dom of C).h = (the Cod of C).g & (the Dom of C).g = (the Cod of C).f holds (the Comp of C).[h,(the Comp of C).[g,f]] = (the Comp of C).[(the Comp of C).[h,g],f] ) & (for b being Element of the Objects of C holds (the Dom of C).((the Id of C).b) = b & (the Cod of C).((the Id of C).b) = b & (for f being Element of the Morphisms of C st (the Cod of C).f = b holds (the Comp of C).[(the Id of C).b,f] = f ) & (for g being Element of the Morphisms of C st (the Dom of C).g = b holds (the Comp of C).[g,(the Id of C).b] = g ) ) by Lm1; then C is Category by Def8; hence thesis; end; end; canceled; theorem for C being CatStr st ( for f,g being Morphism of C holds [g,f] in dom(the Comp of C) iff dom g = cod f ) & ( for f,g being Morphism of C st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g ) & ( for f,g,h being Morphism of C st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f ) & ( for b being Object of C holds dom id b = b & cod id b = b & (for f being Morphism of C st cod f = b holds (id b)*f = f) & (for g being Morphism of C st dom g = b holds g*(id b) = g) ) holds C is Category-like proof let C be CatStr; set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C, CI = the Id of C; assume that A1: for f,g being Morphism of C holds [g,f] in dom CP iff dom g = cod f and A2: for f,g being Morphism of C st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g and A3: for f,g,h being Morphism of C st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f and A4: for b being Object of C holds dom id b = b & cod id b = b & (for f being Morphism of C st cod f = b holds (id b)*f = f) & (for g being Morphism of C st dom g = b holds g*(id b) = g); thus A5: for f,g being Element of the Morphisms of C holds [g,f] in dom CP iff CD.g=CC.f proof let f,g be Element of the Morphisms of C; CD.g = dom g & CC.f = cod f by Def2,Def3; hence thesis by A1; end; thus A6: for f,g being Element of the Morphisms of C st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g proof let f,g be Element of the Morphisms of C such that A7: CD.g=CC.f; CD.g = dom g & CC.f = cod f by Def2,Def3; then dom(g*f)=dom f & cod(g*f)=cod g & [g,f] in dom CP & CD.(g*f) = dom(g*f) & CC.(g*f) = cod(g*f) by A2,A5,A7,Def2,Def3; then CD.(CP.[g,f]) = dom f & CC.(CP.[g,f]) = cod g by Def4; hence thesis by Def2,Def3; end; thus for f,g,h being Element of the Morphisms of C st CD.h = CC.g & CD.g = CC.f holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f] proof let f,g,h be Element of the Morphisms of C such that A8: CD.h = CC.g & CD.g = CC.f; A9: CD.h = dom h & CC.g = cod g & CD.g = dom g & CC.f = cod f by Def2,Def3; [g,f] in dom CP & [h,g] in dom CP by A5,A8; then A10: g*f = CP.[g,f] & h*g = CP.[h,g] by Def4; CD.(CP.[h,g]) = CD.g & CC.(CP.[g,f]) = CC.g by A6,A8; then [h,g*f] in dom CP & [h*g,f] in dom CP by A5,A8,A10; then CP.[h,g*f] = h*(g*f) & CP.[h*g,f] = (h*g)*f by Def4; hence thesis by A3,A8,A9,A10; end; let b be Element of the Objects of C; dom id b = b & cod id b = b & id b = CI.b by A4,Def5; hence CD.(CI.b) = b & CC.(CI.b) = b by Def2,Def3; thus for f being Element of the Morphisms of C st CC.f = b holds CP.[CI.b,f] = f proof let f be Element of the Morphisms of C such that A11: CC.f = b; A12: dom id b = b & id b = CI.b by A4,Def5; then CD.(CI.b) = b & CC.f = cod f by Def2,Def3; then (id b)*f = f & [CI.b,f] in dom CP by A4,A5,A11; hence thesis by A12,Def4; end; let g be Element of the Morphisms of C such that A13: CD.g = b; A14: cod id b = b & id b = CI.b by A4,Def5; then CC.(CI.b) = b & CD.g = dom g by Def2,Def3; then g*(id b) = g & [g,CI.b] in dom CP by A4,A5,A13; hence thesis by A14,Def4; end; definition let o,m; func 1Cat(o,m) -> strict Category equals :Def9: CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #); correctness proof consider O,M being non empty set,d,c being (Function of M,O), p being (PartFunc of [:M,M:],M),i being (Function of O,M), C being CatStr such that A1: O = {o} & M = {m} & d = {m}-->o & c = {m}-->o & p = (m,m).-->m & i = {o}-->m & C = CatStr(# {o},{m},{m}-->o,{m}-->o, (m,m).-->m,{o}-->m #); (for f,g being Element of the Morphisms of C holds [g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f) & (for f,g being Element of the Morphisms of C st (the Dom of C).g=(the Cod of C).f holds (the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f & (the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g) & (for f,g,h being Element of the Morphisms of C st (the Dom of C).h = (the Cod of C).g & (the Dom of C).g = (the Cod of C).f holds (the Comp of C).[h,(the Comp of C).[g,f]] = (the Comp of C).[(the Comp of C).[h,g],f] ) & (for b being Element of the Objects of C holds (the Dom of C).((the Id of C).b) = b & (the Cod of C).((the Id of C).b) = b & (for f being Element of the Morphisms of C st (the Cod of C).f = b holds (the Comp of C).[(the Id of C).b,f] = f ) & (for g being Element of the Morphisms of C st (the Dom of C).g = b holds (the Comp of C).[g,(the Id of C).b] = g ) ) by A1,Lm1; hence thesis by A1,Def8; end; end; canceled 2; theorem o is Object of 1Cat(o,m) proof 1Cat(o,m) = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9; hence thesis by TARSKI:def 1; end; theorem m is Morphism of 1Cat(o,m) proof 1Cat(o,m)=CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9; hence thesis by TARSKI:def 1; end; theorem Th34: for a being Object of 1Cat(o,m) holds a = o proof let a be Object of 1Cat(o,m); 1Cat(o,m) = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9; hence thesis by TARSKI:def 1; end; theorem Th35: for f being Morphism of 1Cat(o,m) holds f = m proof let f be Morphism of 1Cat(o,m); 1Cat(o,m) = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9; hence thesis by TARSKI:def 1; end; theorem Th36: for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m) holds f in Hom(a,b) proof let a,b be Object of 1Cat(o,m); let f be Morphism of 1Cat(o,m); dom f = o & cod f = o by Th34; then dom f = a & cod f = b by Th34; hence f in Hom(a,b) by Th18; end; theorem for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m) holds f is Morphism of a,b proof let a,b be Object of 1Cat(o,m); let f be Morphism of 1Cat(o,m); f in Hom(a,b) by Th36; hence thesis by Def7; end; theorem for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {} by Th36; theorem for a,b,c,d being Object of 1Cat(o,m) for f being Morphism of a,b for g being Morphism of c,d holds f=g proof let a,b,c,d be Object of 1Cat(o,m); let f be Morphism of a,b; let g be Morphism of c,d; f = m & g = m by Th35; hence thesis; end; reserve B,C,D for Category; reserve a,b,c,d for Object of C; reserve f,f1,f2,g,g1,g2 for Morphism of C; theorem Th40: dom(g) = cod(f) iff [g,f] in dom(the Comp of C) proof dom(g) = (the Dom of C).g & cod(f) = (the Cod of C).f by Def2,Def3; hence thesis by Def8; end; theorem Th41: dom(g) = cod(f) implies g*f = ( the Comp of C ).[g,f] proof assume dom(g) = cod(f); then [g,f] in dom(the Comp of C) by Th40; hence g*f = ( the Comp of C ).[g,f] by Def4; end; theorem Th42: for f,g being Morphism of C st dom(g) = cod(f) holds dom(g*f) = dom(f) & cod(g*f) = cod(g) proof let f,g be Morphism of C; assume A1: dom(g) = cod(f); then dom(g) = (the Dom of C).g & cod(g) = (the Cod of C).g & dom(f) = (the Dom of C).f & cod(f) = (the Cod of C).f & (the Dom of C).(g*f) = dom(g*f) & (the Cod of C).(g*f) = cod(g*f) & (the Comp of C).[g,f] = g*f by Def2,Def3,Th41; hence thesis by A1,Def8; end; theorem Th43: for f,g,h being Morphism of C st dom(h) = cod(g) & dom(g) = cod(f) holds h*(g*f) = (h*g)*f proof let f,g,h be Morphism of C; assume A1: dom(h) = cod(g) & dom(g) = cod(f); then cod(g*f) = cod(g) & dom(h*g) = dom(g) by Th42; then dom(g) = (the Dom of C).g & cod(g) = (the Cod of C).g & dom(h) = (the Dom of C).h & cod(f) = (the Cod of C).f & (the Dom of C).(g*f) = dom(g*f) & (the Cod of C).(g*f) = cod(g*f) & (the Comp of C).[h,g*f] = h*(g*f) & (the Comp of C).[h*g,f] = (h*g)*f & (the Comp of C).[h,g] = h*g & (the Comp of C).[g,f] = g*f by A1,Def2,Def3,Th41; hence thesis by A1,Def8; end; theorem Th44: dom(id b) = b & cod(id b) = b proof dom(id b) = (the Dom of C).(id b) & cod(id b) = (the Cod of C).(id b) & id b = (the Id of C).b by Def2,Def3,Def5; hence thesis by Def8; end; theorem Th45: id a = id b implies a = b proof dom id a = a & dom id b = b by Th44; hence thesis; end; theorem Th46: for f being Morphism of C st cod(f) = b holds (id b)*f = f proof let f be Morphism of C; assume A1: cod(f) = b; then dom(id b) = cod(f) by Th44; then cod(f) = (the Cod of C).f & id b = (the Id of C).b & (the Comp of C).[id b,f] = (id b)*f by Def3,Def5,Th41; hence thesis by A1,Def8; end; theorem Th47: for g being Morphism of C st dom(g) = b holds g*(id b) = g proof let g be Morphism of C; assume A1: dom(g) = b; then cod(id b) = dom(g) by Th44; then dom(g) = (the Dom of C).g & id b = (the Id of C).b & (the Comp of C).[g,id b] = g*(id b) by Def2,Def5,Th41; hence thesis by A1,Def8; end; definition let C,g; attr g is monic means for f1,f2 st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g*f1=g*f2 holds f1=f2; end; definition let C,f; attr f is epi means for g1,g2 st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f=g2*f holds g1=g2; end; definition let C,f; attr f is invertible means ex g st dom g = cod f & cod g = dom f & f*g = id cod f & g*f = id dom f; end; reserve f,f1,f2 for Morphism of a,b; reserve f' for Morphism of b,a; reserve g for Morphism of b,c; reserve h,h1,h2 for Morphism of c,d; canceled 3; theorem Th51: Hom(a,b)<>{} & Hom(b,c)<>{} implies g*f in Hom(a,c) proof assume Hom(a,b)<>{} & Hom(b,c)<>{}; then f in Hom(a,b) & g in Hom(b,c) by Def7; then dom(g)=b & cod(g)=c & dom(f)=a & cod(f)=b by Th18; then dom(g*f) = a & cod(g*f) = c by Th42; hence (g*f) in Hom(a,c) by Th18; end; theorem Hom(a,b)<>{} & Hom(b,c)<>{} implies Hom(a,c)<>{} by Th51; definition let C,a,b,c,f,g; assume A1: Hom(a,b)<>{} & Hom(b,c)<>{}; func g*f -> Morphism of a,c equals :Def13: g*f; correctness proof g*f in Hom(a,c) by A1,Th51; hence thesis by Def7; end; end; canceled; theorem Th54: Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g*f) proof assume that A1: Hom(a,b)<>{} and A2: Hom(b,c)<>{} and A3: Hom(c,d)<>{}; reconsider ff = f as Morphism of C; reconsider gg = g as Morphism of C; reconsider hh = h as Morphism of C; f in Hom(a,b) & g in Hom(b,c) & h in Hom(c,d) by A1,A2,A3,Def7; then A4: dom(h) = c & cod(g) = c & dom(g) = b & cod(f) = b by Th18; A5: Hom(a,c)<>{} by A1,A2,Th51; Hom(b,d) <> {} by A2,A3,Th51; hence (h*g)*f = (h*g)*ff by A1,Def13 .= (hh*gg)*ff by A2,A3,Def13 .= hh*(gg*ff) by A4,Th43 .= hh*(g*f) by A1,A2,Def13 .= h*(g*f) by A3,A5,Def13; end; theorem Th55: id a in Hom(a,a) proof dom(id a)=a & cod(id a)=a by Th44; hence thesis by Th18; end; theorem Hom(a,a) <> {} by Th55; definition let C,a; redefine func id a -> Morphism of a,a; coherence proof id a in Hom(a,a) by Th55; hence id a is Morphism of a,a by Def7; end; end; theorem Th57: Hom(a,b)<>{} implies (id b)*f=f proof assume A1: Hom(a,b)<>{}; then f in Hom(a,b) by Def7; then cod(f) = b by Th18; then (id b)*(f qua Morphism of C) = f & Hom(b,b) <> {} by Th46,Th55; hence (id b)*f = f by A1,Def13; end; theorem Th58: Hom(b,c)<>{} implies g*(id b)=g proof assume A1: Hom(b,c)<>{}; then g in Hom(b,c) by Def7; then dom(g) = b by Th18; then g*((id b) qua Morphism of C) = g & Hom(b,b) <> {} by Th47,Th55; hence g*(id b) = g by A1,Def13; end; theorem Th59: (id a)*(id a) = id a proof Hom(a,a) <> {} by Th55; hence thesis by Th57; end; :: Monics, Epis theorem Th60: Hom(b,c) <> {} implies (g is monic iff for a for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2) proof assume A1: Hom(b,c) <> {}; thus g is monic implies for a for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2 proof assume A2: for f1,f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g*f1=g*f2 holds f1=f2; let a; let f1,f2 be Morphism of a,b; assume Hom(a,b)<>{}; then dom f1 = a & dom f2 = a & cod f1 = b & cod f2 = b & dom g = b & g*f2 = g*(f2 qua Morphism of C) & g*f1 = g*(f1 qua Morphism of C) by A1,Def13,Th23; hence thesis by A2; end; assume A3: for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2; let f1,f2 be Morphism of C such that A4: dom f1 = dom f2 and A5: cod f1 = dom g and A6: cod f2 = dom g; A7: dom g = b by A1,Th23; set a = dom(f1); reconsider f1 as Morphism of a,b by A5,A7,Th22; reconsider f2 as Morphism of a,b by A4,A6,A7,Th22; A8: Hom(a,b) <> {} by A5,A7,Th18; then g*f2 = g*(f2 qua Morphism of C) & g*f1 = g*(f1 qua Morphism of C) by A1,Def13; hence thesis by A3,A8; end; theorem Hom(b,c)<>{} & Hom(c,d)<>{} & g is monic & h is monic implies h*g is monic proof assume that A1: Hom(b,c)<>{} & Hom(c,d)<>{} and A2: g is monic and A3: h is monic; A4: Hom(b,d) <> {} by A1,Th51; now let a,f1,f2 such that A5: Hom(a,b)<>{} and A6: (h*g)*f1 = (h*g)*f2; h*(g*f1) = (h*g)*f1 & (h*g)*f2 = h*(g*f2) & Hom(a,c) <> {} by A1,A5,Th51,Th54; then g*f1 = g*f2 by A1,A3,A6,Th60; hence f1 = f2 by A1,A2,A5,Th60; end; hence thesis by A4,Th60; end; theorem Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic proof assume that A1: Hom(b,c)<>{} & Hom(c,d)<>{} and A2: h*g is monic; now let a,f1,f2; assume A3: Hom(a,b)<>{}; then Hom(b,d) <> {} & h*(g*f1) = (h*g)*f1 & h*(g*f2) = (h*g)*f2 by A1,Th51,Th54; hence g*f1 = g*f2 implies f1 = f2 by A2,A3,Th60; end; hence thesis by A1,Th60; end; theorem for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <> {} & Hom(b,a) <> {} & h*g = id b holds g is monic proof let h be Morphism of a,b; let g be Morphism of b,a such that A1: Hom(a,b) <> {} and A2: Hom(b,a) <> {} and A3: h*g = id b; now let c; let g1,g2 be Morphism of c,b such that A4: Hom(c,b) <> {} and A5: g*g1 = g*g2; thus g1 = (h*g)*g1 by A3,A4,Th57 .= h*(g*g2) by A1,A2,A4,A5,Th54 .= (h*g)*g2 by A1,A2,A4,Th54 .= g2 by A3,A4,Th57; end; hence thesis by A2,Th60; end; theorem id b is monic proof A1: Hom(b,b) <> {} by Th55; now let a; let f1,f2 be Morphism of a,b; assume Hom(a,b)<>{}; then (id b)*f1 = f1 & (id b)*f2 = f2 by Th57; hence (id b)*f1 = (id b)*f2 implies f1 = f2; end; hence thesis by A1,Th60; end; theorem Th65: Hom(a,b) <> {} implies (f is epi iff for c for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2) proof assume A1: Hom(a,b) <> {}; thus f is epi implies for c for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2 proof assume A2: for g1,g2 being Morphism of C st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f = g2*f holds g1=g2; let c; let g1,g2 be Morphism of b,c; assume Hom(b,c)<>{}; then dom g1 = b & dom g2 = b & cod g1 = c & cod g2 = c & cod f = b & g1*f = g1*(f qua Morphism of C) & g2*f = g2*(f qua Morphism of C) by A1,Def13,Th23; hence thesis by A2; end; assume A3: for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2; let g1,g2 be Morphism of C such that A4: dom g1 = cod f and A5: dom g2 = cod f and A6: cod g1 = cod g2; A7: cod f = b by A1,Th23; set c = cod g1; reconsider g1 as Morphism of b,c by A4,A7,Th22; reconsider g2 as Morphism of b,c by A5,A6,A7,Th22; A8: Hom(b,c) <> {} by A4,A7,Th18; then g1*f = g1*(f qua Morphism of C) & g2*f = g2*(f qua Morphism of C) by A1,Def13; hence thesis by A3,A8; end; theorem Hom(a,b)<>{} & Hom(b,c)<>{} & f is epi & g is epi implies g*f is epi proof assume that A1: Hom(a,b)<>{} & Hom(b,c)<>{} and A2: f is epi and A3: g is epi; A4: Hom(a,c) <> {} by A1,Th51; now let d,h1,h2 such that A5: Hom(c,d)<>{} and A6: h1*(g*f) = h2*(g*f); h1*(g*f) = (h1*g)*f & (h2*g)*f = h2*(g*f) & Hom(b,d) <> {} by A1,A5,Th51,Th54; then h1*g = h2*g by A1,A2,A6,Th65; hence h1 = h2 by A1,A3,A5,Th65; end; hence thesis by A4,Th65; end; theorem Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi proof assume that A1: Hom(a,b)<>{} & Hom(b,c)<>{} and A2: g*f is epi; now let d,h1,h2; assume A3: Hom(c,d)<>{}; then Hom(a,c) <> {} & h1*(g*f) = (h1*g)*f & h2*(g*f) = (h2*g)*f by A1,Th51,Th54; hence h1*g = h2*g implies h1 = h2 by A2,A3,Th65; end; hence thesis by A1,Th65; end; theorem for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <> {} & Hom(b,a) <> {} & h*g = id b holds h is epi proof let h be Morphism of a,b; let g be Morphism of b,a; assume that A1: Hom(a,b) <> {} and A2: Hom(b,a) <> {} and A3: h*g = id b; now let c; let h1,h2 be Morphism of b,c such that A4: Hom(b,c) <> {} and A5: h1*h = h2*h; thus h1 = h1*(h*g) by A3,A4,Th58 .= (h2*h)*g by A1,A2,A4,A5,Th54 .= h2*(h*g) by A1,A2,A4,Th54 .= h2 by A3,A4,Th58; end; hence thesis by A1,Th65; end; theorem id b is epi proof A1: Hom(b,b) <> {} by Th55; now let c; let g1,g2 be Morphism of b,c; assume Hom(b,c)<>{}; then g1*(id b) = g1 & g2*(id b) = g2 by Th58; hence g1*(id b) = g2*(id b) implies g1 = g2; end; hence thesis by A1,Th65; end; theorem Th70: Hom(a,b) <> {} implies (f is invertible iff Hom(b,a)<>{} & ex g being Morphism of b,a st f*g=id b & g*f=id a) proof assume A1: Hom(a,b) <> {}; thus f is invertible implies Hom(b,a)<>{} & ex g being Morphism of b,a st f*g=id b & g*f=id a proof given g being Morphism of C such that A2: dom g = cod f & cod g = dom f and A3: f*g = id cod f & g*f = id dom f; A4: dom f = a & cod f = b by A1,Th23; hence A5: Hom(b,a) <> {} by A2,Th18; reconsider g as Morphism of b,a by A2,A4,Th22; take g; thus thesis by A1,A3,A4,A5,Def13; end; assume A6: Hom(b,a)<>{}; given g being Morphism of b,a such that A7: f*g=id b & g*f=id a; reconsider g as Morphism of C; take g; dom f = a & cod g = a & cod f = b & dom g = b by A1,A6,Th23; hence thesis by A1,A6,A7,Def13; end; theorem Th71: Hom(a,b) <> {} & Hom(b,a) <> {} implies for g1,g2 being Morphism of b,a st f*g1=id b & g2*f=id a holds g1=g2 proof assume that A1: Hom(a,b) <> {} and A2: Hom(b,a) <> {}; let g1,g2 be Morphism of b,a; assume A3: f*g1=id b; assume g2*f=id a; hence g1 = (g2*f)*g1 by A2,Th57 .= g2*(id b) by A1,A2,A3,Th54 .= g2 by A2,Th58; end; definition let C,a,b,f; assume that A1: Hom(a,b) <> {} and A2: f is invertible; func f" -> Morphism of b,a means :Def14: f*it = id b & it*f = id a; existence by A1,A2,Th70; uniqueness proof Hom(b,a) <> {} by A1,A2,Th70; hence thesis by A1,Th71; end; end; canceled; theorem Hom(a,b)<>{} & f is invertible implies f is monic & f is epi proof assume that A1: Hom(a,b)<>{} and A2: f is invertible; A3: Hom(b,a)<>{} by A1,A2,Th70; consider k being Morphism of b,a such that A4: f*k=id b and A5: k*f=id a by A1,A2,Th70; now let c be (Object of C),g,h be Morphism of c,a such that A6: Hom(c,a)<>{} and A7: f*g=f*h; g = (k*f)*g by A5,A6,Th57 .= k*(f*h) by A1,A3,A6,A7,Th54 .= (id a)*h by A1,A3,A5,A6,Th54; hence g=h by A6,Th57; end; hence f is monic by A1,Th60; now let c be (Object of C), g,h be Morphism of b,c such that A8: Hom(b,c)<>{} and A9: g*f=h*f; g = g*(f*k) by A4,A8,Th58 .= (h*f)*k by A1,A3,A8,A9,Th54 .= h*(id b) by A1,A3,A4,A8,Th54; hence g=h by A8,Th58; end; hence f is epi by A1,Th65; end; theorem id a is invertible proof Hom(a,a) <> {} & (id a)*(id a) = id a by Th55,Th59; hence thesis by Th70; end; theorem Th75: Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible implies g*f is invertible proof assume that A1: Hom(a,b) <> {} and A2: Hom(b,c) <> {}; assume A3: f is invertible; then A4: Hom(b,a) <> {} by A1,Th70; consider f1 being Morphism of b,a such that A5: f*f1 = id b and A6: f1*f = id a by A1,A3,Th70; assume A7: g is invertible; then A8: Hom(c,b) <> {} by A2,Th70; consider g1 being Morphism of c,b such that A9: g*g1 = id c and A10: g1*g = id b by A2,A7,Th70; A11: Hom(a,c) <> {} by A1,A2,Th51; now thus A12: Hom(c,a) <> {} by A4,A8,Th51; take f1g1 = f1*g1; thus (g*f)*(f1g1) = g*(f*(f1*g1)) by A1,A2,A12,Th54 .= g*((id b )*g1) by A1,A4,A5,A8,Th54 .= id c by A8,A9,Th57; Hom(a,c) <> {} by A1,A2,Th51; hence (f1g1)*(g*f) = f1*(g1*(g*f)) by A4,A8,Th54 .= f1*((id b)*f) by A1,A2,A8,A10,Th54 .= id a by A1,A6,Th57; end; hence thesis by A11,Th70; end; theorem Hom(a,b)<>{} & f is invertible implies f" is invertible proof assume A1: Hom(a,b) <> {}; assume f is invertible; then Hom(b,a) <> {} & (f")*f = id a & f*(f") = id b by A1,Def14,Th70; hence thesis by A1,Th70; end; theorem Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible implies (g*f)" = f"*g" proof assume that A1: Hom(a,b) <> {} and A2: Hom(b,c) <> {} and A3: f is invertible and A4: g is invertible; now thus Hom(a,c) <> {} by A1,A2,Th51; thus g*f is invertible by A1,A2,A3,A4,Th75; A5: Hom(b,a) <> {} by A1,A3,Th70; A6: Hom(c,b) <> {} by A2,A4,Th70; then A7: Hom(c,a) <> {} by A5,Th51; hence (g*f)*(f"*g") = g*(f*(f"*g")) by A1,A2,Th54 .= g*((f*f")*g") by A1,A5,A6,Th54 .= g*((id b)*g") by A1,A3,Def14 .= g*g" by A6,Th57 .= id c by A2,A4,Def14; thus (f"*g")*(g*f) = ((f"*g")*g)*f by A1,A2,A7,Th54 .= (f"*(g"*g))*f by A2,A5,A6,Th54 .= (f"*(id b))*f by A2,A4,Def14 .= f"*f by A5,Th58 .= id a by A1,A3,Def14; end; hence thesis by Def14; end; definition let C,a; attr a is terminal means :Def15: Hom(b,a)<>{} & ex f being Morphism of b,a st for g being Morphism of b,a holds f=g; attr a is initial means :Def16: Hom(a,b)<>{} & ex f being Morphism of a,b st for g being Morphism of a,b holds f=g; let b; pred a,b are_isomorphic means :Def17: Hom(a,b)<>{} & ex f st f is invertible; end; canceled 3; theorem Th81: a,b are_isomorphic iff Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f' st f*f' = id b & f'*f = id a proof thus a,b are_isomorphic implies Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f' st f*f' = id b & f'*f = id a proof assume A1: Hom(a,b) <> {}; given f such that A2: f is invertible; thus Hom(a,b) <> {} & Hom(b,a) <> {} by A1,A2,Th70; take f; thus thesis by A1,A2,Th70; end; assume that A3: Hom(a,b)<>{} and A4: Hom(b,a)<>{}; given f such that A5: ex f' st f*f' = id b & f'*f = id a; thus Hom(a,b) <> {} by A3; take f; thus thesis by A3,A4,A5,Th70; end; theorem a is initial iff for b ex f being Morphism of a,b st Hom(a,b) = {f} proof thus a is initial implies for b ex f being Morphism of a,b st Hom(a,b) = {f} proof assume A1: a is initial; let b; consider f being Morphism of a,b such that A2: for g being Morphism of a,b holds f = g by A1,Def16; take f; Hom(a,b) <> {} by A1,Def16; hence thesis by A2,Th26; end; assume A3: for b ex f being Morphism of a,b st Hom(a,b) = {f}; let b; consider f being Morphism of a,b such that A4: Hom(a,b) = {f} by A3; thus Hom(a,b) <> {} by A4; take f; thus thesis by A4,Th25; end; theorem Th83: a is initial implies for h being Morphism of a,a holds id a = h proof assume a is initial; then consider f being Morphism of a,a such that A1: for g being Morphism of a,a holds f = g by Def16; let h be Morphism of a,a; id a = f by A1; hence thesis by A1; end; theorem a is initial & b is initial implies a,b are_isomorphic proof assume that A1: a is initial and A2: b is initial; thus A3: Hom(a,b) <> {} by A1,Def16; consider f being Morphism of a,b; consider g being Morphism of b,a; take f; now thus Hom(b,a) <> {} by A2,Def16; take g; thus f*g = id b & g*f = id a by A1,A2,Th83; end; hence thesis by A3,Th70; end; theorem a is initial & a,b are_isomorphic implies b is initial proof assume that A1: a is initial and A2: a,b are_isomorphic; let c; consider h being Morphism of a,c such that A3: for g being Morphism of a,c holds h = g by A1,Def16; consider f,f' such that A4: f*f' = id b and f'*f = id a by A2,Th81; A5: Hom(b,a) <> {} by A2,Th81; Hom(a,c) <> {} by A1,Def16; hence A6: Hom(b,c) <> {} by A5,Th51; take h*f'; A7: Hom(a,b) <> {} by A2,Def17; let h' be Morphism of b,c; thus h' = h'*(f*f') by A4,A6,Th58 .= (h'*f)*f' by A5,A6,A7,Th54 .= h*f' by A3; end; theorem b is terminal iff for a ex f being Morphism of a,b st Hom(a,b) = {f} proof thus b is terminal implies for a ex f being Morphism of a,b st Hom(a,b) = {f} proof assume A1: b is terminal; let a; consider f being Morphism of a,b such that A2: for g being Morphism of a,b holds f = g by A1,Def15; take f; Hom(a,b) <> {} by A1,Def15; hence thesis by A2,Th26; end; assume A3: for a ex f being Morphism of a,b st Hom(a,b) = {f}; let a; consider f being Morphism of a,b such that A4: Hom(a,b) = {f} by A3; thus Hom(a,b) <> {} by A4; take f; thus thesis by A4,Th25; end; theorem Th87: a is terminal implies for h being Morphism of a,a holds id a = h proof assume a is terminal; then consider f being Morphism of a,a such that A1: for g being Morphism of a,a holds f = g by Def15; let h be Morphism of a,a; id a = f by A1; hence thesis by A1; end; theorem a is terminal & b is terminal implies a,b are_isomorphic proof assume that A1: a is terminal and A2: b is terminal; thus A3: Hom(a,b) <> {} by A2,Def15; consider f being Morphism of a,b; consider g being Morphism of b,a; take f; now thus Hom(b,a) <> {} by A1,Def15; take g; thus f*g = id b & g*f = id a by A1,A2,Th87; end; hence thesis by A3,Th70; end; theorem b is terminal & a,b are_isomorphic implies a is terminal proof assume that A1: b is terminal and A2: a,b are_isomorphic; let c; consider h being Morphism of c,b such that A3: for g being Morphism of c,b holds h = g by A1,Def15; consider f,f' such that f*f' = id b and A4: f'*f = id a by A2,Th81; A5: Hom(b,a) <> {} by A2,Th81; Hom(c,b) <> {} by A1,Def15; hence A6: Hom(c,a) <> {} by A5,Th51; take f'*h; A7: Hom(a,b) <> {} by A2,Def17; let h' be Morphism of c,a; thus f'*h = f'*(f*h') by A3 .= (f'*f)*h' by A5,A6,A7,Th54 .= h' by A4,A6,Th57; end; theorem Hom(a,b) <> {} & a is terminal implies f is monic proof assume that A1: Hom(a,b) <> {} and A2: a is terminal; now let c be (Object of C),g,h be Morphism of c,a such that Hom(c,a)<>{} and f*g=f*h; consider ff being Morphism of c,a such that A3: for gg being Morphism of c,a holds ff=gg by A2,Def15; ff = g by A3; hence g=h by A3; end; hence thesis by A1,Th60; end; theorem a,a are_isomorphic proof thus A1: Hom(a,a) <> {} by Th55; take id a; (id a)*(id a) = id a by Th59; hence thesis by A1,Th70; end; theorem a,b are_isomorphic implies b,a are_isomorphic proof assume A1: Hom(a,b) <> {}; given f being Morphism of a,b such that A2: f is invertible; thus A3: Hom(b,a) <> {} by A1,A2,Th70; consider g being Morphism of b,a such that A4: f*g = id b & g*f = id a by A1,A2,Th70; take g; thus thesis by A1,A3,A4,Th70; end; theorem a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic proof assume A1: Hom(a,b) <> {}; given f being Morphism of a,b such that A2: f is invertible; assume A3: Hom(b,c) <> {}; given g being Morphism of b,c such that A4: g is invertible; thus Hom(a,c) <> {} by A1,A3,Th51; take g*f; thus thesis by A1,A2,A3,A4,Th75; end; :: Functors (Covariant Functors) definition let C,D; mode Functor of C,D -> Function of the Morphisms of C,the Morphisms of D means :Def18: ( for c being Element of the Objects of C ex d being Element of the Objects of D st it.((the Id of C).c) = (the Id of D).d ) & ( for f being Element of the Morphisms of C holds it.((the Id of C).((the Dom of C).f)) = (the Id of D).((the Dom of D).(it.f)) & it.((the Id of C).((the Cod of C).f)) = (the Id of D).((the Cod of D).(it.f)) ) & ( for f,g being Element of the Morphisms of C st [g,f] in dom(the Comp of C) holds it.((the Comp of C).[g,f]) = (the Comp of D).[it.g,it.f] ); existence proof consider d being Element of the Objects of D; deffunc F(set) = (the Id of D).d; consider F being Function of the Morphisms of C,the Morphisms of D such that A1: for f being Element of the Morphisms of C holds F.f = F(f) from LambdaD; take F; thus for c being Element of the Objects of C ex d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d proof let c be Element of the Objects of C; take d; thus thesis by A1; end; thus for f being Element of the Morphisms of C holds F.((the Id of C).((the Dom of C).f)) = (the Id of D).((the Dom of D).(F.f)) & F.((the Id of C).((the Cod of C).f)) = (the Id of D).((the Cod of D).(F.f)) proof let f be Element of the Morphisms of C; A2: F.f = (the Id of D).d by A1; thus F.((the Id of C).((the Dom of C).f)) = (the Id of D).d by A1 .= (the Id of D).((the Dom of D).(F.f)) by A2,Def8; thus F.((the Id of C).((the Cod of C).f)) = (the Id of D).d by A1 .= (the Id of D).((the Cod of D).(F.f)) by A2,Def8; end; let f,g be Element of the Morphisms of C such that A3: [g,f] in dom(the Comp of C); set f' = F.f; A4: (the Id of D).d = id d by Def5; F.g = (the Id of D).d & F.f = (the Id of D).d by A1; then (the Dom of D).(F.g) = d & (the Cod of D).(F.f) = d by Def8; then A5: [F.g,F.f] in dom(the Comp of D) by Def8; A6: Hom(d,d) <> {} by Th55; (the Comp of C).[g,f] is Element of the Morphisms of C by A3,PARTFUN1:27; hence F.((the Comp of C).[g,f]) = (the Id of D).d by A1 .= (id d)*(id d) by A4,Th59 .= (id d)*((id d) qua Morphism of D) by A6,Def13 .= (id d)*f' by A1,A4 .= F.g*f' by A1,A4 .= (the Comp of D).[F.g,F.f] by A5,Def4; end; end; canceled 2; theorem Th96: for T being Function of the Morphisms of C,the Morphisms of D st ( 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)) holds T is Functor of C,D proof let T be Function of the Morphisms of C,the Morphisms of D such that A1: for c being Object of C ex d being Object of D st T.(id c) = id d and A2: for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) and A3: for f,g being Morphism of C st dom g = cod f holds T.(g*f) = (T.g)*(T.f); thus for c being Element of the Objects of C ex d being Element of the Objects of D st T.((the Id of C).c) = (the Id of D).d proof let c be Element of the Objects of C; consider d being Object of D such that A4: T.(id c) = id d by A1; id c = (the Id of C).c & id d = (the Id of D).d by Def5; hence thesis by A4; end; thus for f being Element of the Morphisms of C holds T.((the Id of C).((the Dom of C).f)) = (the Id of D).((the Dom of D).(T.f)) & T.((the Id of C).((the Cod of C).f)) = (the Id of D).((the Cod of D).(T.f)) proof let f be Element of the Morphisms of C; (the Dom of C).f = dom f & (the Id of C).(dom f) = id dom f & (the Dom of D).(T.f) = dom(T.f) & (the Id of D).(dom (T.f)) = id dom(T.f) & (the Cod of C).f = cod f & (the Id of C).(cod f) = id cod f & (the Cod of D).(T.f) = cod(T.f) & (the Id of D).(cod (T.f)) = id cod(T.f) by Def2,Def3,Def5; hence thesis by A2; end; let f,g be Element of the Morphisms of C; assume [g,f] in dom(the Comp of C); then A5: dom g = cod f by Th40; then id dom (T.g) = T.(id cod f) by A2 .= id cod (T.f) by A2; then dom (T.g) = cod (T.f) by Th45; then (the Comp of C).[g,f] = g*f & (the Comp of D).[T.g,T.f] = (T.g)*(T.f) by A5,Th41; hence thesis by A3,A5; end; theorem Th97: for T being Functor of C,D for c being Object of C ex d being Object of D st T.(id c) = id d proof let T be Functor of C,D; let c be Object of C; consider d being Element of the Objects of D such that A1: T.((the Id of C).c) = (the Id of D).d by Def18; id c = (the Id of C).c & id d = (the Id of D).d by Def5; hence thesis by A1; end; theorem Th98: for T being Functor of C,D for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let T be Functor of C,D; let f be Morphism of C; (the Dom of C).f = dom f & (the Id of C).(dom f) = id dom f & (the Dom of D).(T.f) = dom(T.f) & (the Id of D).(dom (T.f)) = id dom(T.f) & (the Cod of C).f = cod f & (the Id of C).(cod f) = id cod f & (the Cod of D).(T.f) = cod(T.f) & (the Id of D).(cod (T.f)) = id cod(T.f) by Def2,Def3,Def5; hence thesis by Def18; end; theorem Th99: for T being Functor of C,D for f,g being Morphism of C st dom g = cod f holds dom(T.g) = cod(T.f) & T.(g*f) = (T.g)*(T.f) proof let T be Functor of C,D; let f,g be Morphism of C; assume A1: dom g = cod f; then id dom (T.g) = T.(id cod f) by Th98 .= id cod (T.f) by Th98; hence dom (T.g) = cod (T.f) by Th45; then (the Comp of C).[g,f] = g*f & (the Comp of D).[T.g,T.f] = (T.g)*(T.f) & [g,f] in dom(the Comp of C) by A1,Th40,Th41; hence thesis by Def18; end; theorem Th100: for T being Function of the Morphisms of C,the Morphisms of D for F being Function of the Objects of C, the Objects of D st ( for c being Object of C holds T.(id c) = id(F.c) ) & ( for f being Morphism of C holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f) ) & ( for f,g being Morphism of C st dom g = cod f holds T.(g*f) = (T.g)*(T.f)) holds T is Functor of C,D proof let T be Function of the Morphisms of C,the Morphisms of D; let F be Function of the Objects of C, the Objects of D; assume that A1: for c being Object of C holds T.(id c) = id(F.c) and A2: for f being Morphism of C holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f) and A3: for f,g being Morphism of C st dom g = cod f holds T.(g*f) = (T.g)*(T.f); now thus for c being Object of C ex d being Object of D st T.(id c) = id d proof let c be Object of C; take F.c; thus thesis by A1; end; thus for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) proof let f be Morphism of C; thus T.(id dom f) = id (F.(dom f)) by A1 .= id dom (T.f) by A2; thus T.(id cod f) = id (F.(cod f)) by A1 .= id cod (T.f) by A2; end; end; hence thesis by A3,Th96; end; :: Object Function of a Functor definition let C,D; let F be Function of the Morphisms of C,the Morphisms of D; assume A1: for c being Element of the Objects of C ex d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d; func Obj(F) -> Function of the Objects of C,the Objects of D means :Def19: for c being Element of the Objects of C for d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d holds it.c = d; existence proof defpred P[set,set] means for d being Element of the Objects of D st F.((the Id of C).$1) = (the Id of D).d holds $2 = d; A2: for c being Element of the Objects of C ex y being Element of the Objects of D st P[c,y] proof let c be Element of the Objects of C; consider y being Element of the Objects of D such that A3: F.((the Id of C).c) = (the Id of D).y by A1; take y; let d be Element of the Objects of D; assume A4: F.((the Id of C).c) = (the Id of D).d; id d = (the Id of D).d & id y = (the Id of D).y by Def5; hence y = d by A3,A4,Th45; end; thus ex f being Function of the Objects of C,the Objects of D st for x being Element of the Objects of C holds P[x,f.x] from FuncExD(A2); end; uniqueness proof let F1,F2 be Function of the Objects of C,the Objects of D such that A5: for c being Element of the Objects of C for d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d holds F1.c = d and A6: for c being Element of the Objects of C for d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d holds F2.c = d; for c being Element of the Objects of C holds F1.c = F2.c proof let c be Element of the Objects of C; consider d1 being Element of the Objects of D such that A7: F.((the Id of C).c) = (the Id of D).d1 by A1; consider d2 being Element of the Objects of D such that A8: F.((the Id of C).c) = (the Id of D).d2 by A1; id d1 = (the Id of D).d1 & id d2 = ( the Id of D ).d2 & dom id d1 = d1 & dom id d2 = d2 & c is Object of C by Def5,Th44; then F1.c = d1 & F2.c = d2 & d1 = d2 by A5,A6,A7,A8; hence thesis; end; hence thesis by FUNCT_2:113; end; end; canceled; theorem Th102: for T being Function of the Morphisms of C,the Morphisms of D st for c being Object of C ex d being Object of D st T.(id c) = id d for c being Object of C for d being Object of D st T.(id c) = id d holds (Obj T).c = d proof let T be Function of the Morphisms of C,the Morphisms of D such that A1: for c being Object of C ex d being Object of D st T.(id c) = id d; A2: for c being Element of the Objects of C ex d being Element of the Objects of D st T.((the Id of C).c) = (the Id of D).d proof let c be Element of the Objects of C; consider d being Object of D such that A3: T.(id c) = id d by A1; take d; (the Id of C).c = id c & (the Id of D).d = id d by Def5; hence thesis by A3; end; let c be Object of C; let d be Object of D; (the Id of C).c = id c & (the Id of D).d = id d by Def5; hence thesis by A2,Def19; end; theorem Th103: for T being Functor of C,D for c being Object of C for d being Object of D st T.(id c) = id d holds (Obj T).c = d proof let T be Functor of C,D; for c being Object of C ex d being Object of D st T.(id c) = id d by Th97; hence thesis by Th102; end; theorem Th104: for T being (Functor of C,D),c being Object of C holds T.(id c) = id((Obj T).c) proof let T be (Functor of C,D),c be Object of C; ex d being Object of D st T.(id c) = id d by Th97; hence thesis by Th103; end; theorem Th105: for T being (Functor of C,D), f being Morphism of C holds (Obj T).(dom f) = dom (T.f) & (Obj T).(cod f) = cod (T.f) proof let T be (Functor of C,D), f be Morphism of C; T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) by Th98; hence thesis by Th103; end; definition let C,D be Category; let T be Functor of C,D; let c be Object of C; func T.c -> Object of D equals :Def20: (Obj T).c; correctness; end; canceled; theorem for T being Functor of C,D for c being Object of C for d being Object of D st T.(id c) = id d holds T.c = d proof let T be Functor of C,D; let c be Object of C; let d be Object of D; T.c = (Obj T).c by Def20; hence thesis by Th103; end; theorem Th108: for T being (Functor of C, D),c being Object of C holds T.(id c) = id(T.c) proof let T be (Functor of C, D),c be Object of C; T.c = (Obj T).c by Def20; hence thesis by Th104; end; theorem Th109: for T being (Functor of C, D), f being Morphism of C holds T.(dom f) = dom (T.f) & T.(cod f) = cod (T.f) proof let T be (Functor of C, D), f be Morphism of C; T.(dom f) = (Obj T).(dom f) & T.(cod f) = (Obj T).(cod f) by Def20; hence thesis by Th105; end; theorem Th110: for T being Functor of B,C for S being Functor of C,D holds S*T is Functor of B,D proof let T be Functor of B,C; let S be Functor of C,D; reconsider FF = (Obj S)*(Obj T) as Function of the Objects of B , the Objects of D; reconsider TT = S*T as Function of the Morphisms of B , the Morphisms of D; now thus for b being Object of B holds TT.(id b) = id(FF.b) proof let b be Object of B; thus TT.(id b) = S.(T.(id b)) by FUNCT_2:21 .= S.(id(T.b)) by Th108 .= id((S.(T.b))) by Th108 .= id((S.((Obj T).b))) by Def20 .= id(((Obj S).((Obj T).b))) by Def20 .= id(FF.b) by FUNCT_2:21; end; thus for f being Morphism of B holds FF.(dom f) = dom (TT.f) & FF.(cod f) = cod (TT.f) proof let f be Morphism of B; thus FF.(dom f) = (Obj S).((Obj T).(dom f)) by FUNCT_2:21 .= (Obj S).(dom (T.f)) by Th105 .= (dom (S.(T.f))) by Th105 .= dom (TT.f) by FUNCT_2:21; thus FF.(cod f) = (Obj S).((Obj T).(cod f)) by FUNCT_2:21 .= (Obj S).(cod (T.f)) by Th105 .= (cod (S.(T.f))) by Th105 .= cod (TT.f) by FUNCT_2:21; end; let f,g be Morphism of B; assume A1: dom g = cod f; then A2: dom(T.g) = cod(T.f) by Th99; thus TT.(g*f) = S.(T.(g*f)) by FUNCT_2:21 .= S.((T.g)*(T.f)) by A1,Th99 .= (S.(T.g))*(S.(T.f)) by A2,Th99 .= ((TT.g)*(S.(T.f))) by FUNCT_2:21 .= (TT.g)*(TT.f) by FUNCT_2:21; end; hence thesis by Th100; end; :: Composition of Functors definition let B,C,D; let T be Functor of B,C; let S be Functor of C,D; redefine func S*T -> Functor of B,D; coherence by Th110; end; theorem Th111: id the Morphisms of C is Functor of C,C proof set F = id the Objects of C; set T = id the Morphisms of C; now thus for c being Object of C holds T.(id c) = id(F.c) proof let c be Object of C; F.c = c by FUNCT_1:35; hence thesis by FUNCT_1:35; end; thus for f being Morphism of C holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f) proof let f be Morphism of C; T.f = f by FUNCT_1:35; hence thesis by FUNCT_1:35; end; let f,g be Morphism of C; assume dom g = cod f; thus T.(g*f) = g*f by FUNCT_1:35 .= (T.g)*f by FUNCT_1:35 .= (T.g)*(T.f) by FUNCT_1:35; end; hence thesis by Th100; end; theorem Th112: for T being (Functor of B,C),S being (Functor of C,D),b being Object of B holds (Obj (S*T)).b = (Obj S).((Obj T).b) proof let T be (Functor of B,C),S be (Functor of C,D),b be Object of B; consider d being Object of D such that A1: (S*T).(id b) = id d by Th97; consider c being Object of C such that A2: T.(id b) = id c by Th97; A3: (S*T).(id b) = S.(T.(id b)) by FUNCT_2:21; thus (Obj (S*T)).b = d by A1,Th103 .= (Obj S).c by A1,A2,A3,Th103 .= (Obj S).((Obj T).b) by A2,Th103; end; theorem Th113: for T being Functor of B,C for S being Functor of C,D for b being Object of B holds (S*T).b = S.(T.b) proof let T be Functor of B,C; let S be Functor of C,D; let b be Object of B; thus (S*T).b = (Obj (S*T)).b by Def20 .= (Obj S).((Obj T).b) by Th112 .= (Obj S).(T.b) by Def20 .= S.(T.b) by Def20; end; :: Identity Functor definition let C; func id C -> Functor of C,C equals :Def21: id the Morphisms of C; coherence by Th111; end; canceled; theorem Th115: for f being Morphism of C holds (id C).f = f proof let f be Morphism of C; thus (id C).f = (id the Morphisms of C).f by Def21 .= f by FUNCT_1:35; end; theorem Th116: for c being Object of C holds (Obj id C).c = c proof let c be Object of C; (id C).(id c) = id c by Th115; hence (Obj id C).c = c by Th103; end; theorem Th117: Obj id C = id the Objects of C proof dom Obj id C = the Objects of C & for x be set holds x in the Objects of C implies (Obj id C).x = x by Th116,FUNCT_2:def 1; hence thesis by FUNCT_1:34; end; theorem for c being Object of C holds (id C).c = c proof let c be Object of C; (Obj id C).c = c by Th116; hence thesis by Def20; end; definition let C,D be Category; let T be Functor of C,D; attr T is isomorphic means T is one-to-one & rng T = the Morphisms of D & rng Obj T = the Objects of D ; synonym T is_an_isomorphism; attr T is full means :Def23: for c,c' being Object of C st Hom(T.c,T.c') <> {} for g being Morphism of T.c,T.c' holds Hom(c,c') <> {} & ex f being Morphism of c,c' st g = T.f; attr T is faithful means :Def24: for c,c' being Object of C st Hom(c,c') <> {} for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2; end; canceled 3; theorem id C is_an_isomorphism proof rng id the Morphisms of C = the Morphisms of C & rng id the Objects of C = the Objects of C & id the Morphisms of C is one-to-one by FUNCT_1:52,RELAT_1:71; hence id C is one-to-one & rng id C = the Morphisms of C & rng Obj id C = the Objects of C by Def21,Th117; end; theorem Th123: for T being Functor of C,D for c,c' being Object of C for f being set st f in Hom(c,c') holds T.f in Hom(T.c,T.c') proof let T be Functor of C,D; let c,c' be Object of C; let f be set; assume A1: f in Hom(c,c'); then reconsider f' = f as Morphism of c,c' by Def7; dom f' = c & cod f' = c' by A1,Th18; then T.c = dom (T.f') & T.c' = cod(T.f') by Th109; hence T.f in Hom(T.c,T.c') by Th18; end; theorem Th124: for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} for f being Morphism of c,c' holds T.f in Hom(T.c,T.c') proof let T be Functor of C,D; let c,c' be Object of C such that A1: Hom(c,c') <> {}; let f be Morphism of c,c'; f in Hom(c,c') by A1,Def7; hence thesis by Th123; end; theorem Th125: for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} for f being Morphism of c,c' holds T.f is Morphism of T.c,T.c' proof let T be Functor of C,D; let c,c' be Object of C such that A1: Hom(c,c') <> {}; let f be Morphism of c,c'; T.f in Hom(T.c,T.c') by A1,Th124; hence T.f is Morphism of T.c,T.c' by Def7; end; theorem Th126: for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} holds Hom(T.c,T.c') <> {} proof let T be Functor of C,D; let c,c' be Object of C; assume A1: Hom(c,c') <> {}; consider f being Element of Hom(c,c'); f in Hom(c,c') by A1; hence Hom(T.c,T.c') <> {} by Th123; end; theorem for T being Functor of B,C for S being Functor of C,D st T is full & S is full holds S*T is full proof let T be Functor of B,C; let S be Functor of C,D; assume that A1: T is full and A2: S is full; let b,b' be Object of B such that A3: Hom((S*T).b,(S*T).b') <> {}; let g be Morphism of (S*T).b,(S*T).b'; A4: (S*T).b = S.(T.b) & (S*T).b' = S.(T.b') by Th113; then consider f being Morphism of T.b,T.b' such that A5: g = S.f by A2,A3,Def23; A6: Hom(T.b,T.b') <> {} by A2,A3,A4,Def23; hence Hom(b,b') <> {} by A1,Def23; consider h being Morphism of b,b' such that A7: f = T.h by A1,A6,Def23; take h; thus g = (S*T).h by A5,A7,FUNCT_2:21; end; theorem for T being Functor of B,C for S being Functor of C,D st T is faithful & S is faithful holds S*T is faithful proof let T be Functor of B,C; let S be Functor of C,D; assume that A1: T is faithful and A2: S is faithful; let b,b' be Object of B such that A3: Hom(b,b') <> {}; let f1,f2 be Morphism of b,b'; assume A4: (S*T).f1 = (S*T).f2; Hom(T.b,T.b') <> {} & (S*T).f1 = S.(T.f1) & (S*T).f2 = S.(T.f2) & T.f1 is Morphism of T.b,T.b' & T.f2 is Morphism of T.b,T.b' by A3,Th125,Th126,FUNCT_2:21; then T.f1 = T.f2 by A2,A4,Def24; hence f1 = f2 by A1,A3,Def24; end; theorem Th129: for T being Functor of C,D for c,c' being Object of C holds T.:Hom(c,c') c= Hom(T.c,T.c') proof let T be Functor of C,D; let c,c' be Object of C; let f be set; assume f in T.:Hom(c,c'); then ex g being Element of the Morphisms of C st g in Hom(c,c') & f = T.g by FUNCT_2:116; hence f in Hom(T.c,T.c') by Th123; end; definition let C,D be Category; let T be Functor of C,D; let c,c' be Object of C; func hom(T,c,c') -> Function of Hom(c,c') , Hom(T.c,T.c') equals :Def25: T|Hom(c,c'); correctness proof T is Function of the Morphisms of C, the Morphisms of D & Hom(c,c') c= the Morphisms of C & T.:Hom(c,c') c= Hom(T.c,T.c') by Th129; hence thesis by Th4; end; end; canceled; theorem Th131: for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} for f being Morphism of c,c' holds hom(T,c,c').f = T.f proof let T be Functor of C,D; let c,c' be Object of C; assume A1: Hom(c,c') <> {}; let f be Morphism of c,c'; T is Function of the Morphisms of C,the Morphisms of D & f in Hom(c,c') by A1,Def7; then (T|Hom(c,c')).f = T.f by FUNCT_1:72; hence thesis by Def25; end; theorem for T being Functor of C,D holds T is full iff for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c') proof let T be Functor of C,D; thus T is full implies for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c') proof assume A1: T is full; let c,c' be Object of C; A2: now assume A3: Hom(T.c,T.c') = {}; then Hom(c,c') = {} by Th126; hence rng hom(T,c,c') = Hom(T.c,T.c') by A3,PARTFUN1:54; end; now assume A4: Hom(T.c,T.c') <> {}; for g being set holds g in rng hom(T,c,c') iff g in Hom(T.c,T.c') proof let g be set; thus g in rng hom(T,c,c') implies g in Hom(T.c,T.c') proof assume g in rng hom(T,c,c'); then consider f being set such that A5: f in dom hom(T,c,c') and A6: hom(T,c,c').f = g by FUNCT_1:def 5; f in Hom(c,c') by A4,A5,FUNCT_2:def 1; hence thesis by A4,A6,FUNCT_2:7; end; assume g in Hom(T.c,T.c'); then g is Morphism of T.c,T.c' by Def7; then consider f being Morphism of c,c' such that A7: g = T.f by A1,A4,Def23; A8: Hom(c,c') <> {} by A1,A4,Def23; then f in Hom(c,c') by Def7; then hom(T,c,c').f in rng hom(T,c,c') by A4,FUNCT_2:6; hence g in rng hom(T,c,c') by A7,A8,Th131; end; hence rng hom(T,c,c') = Hom(T.c,T.c') by TARSKI:2; end; hence thesis by A2; end; assume A9: for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c'); let c,c' be Object of C such that A10: Hom(T.c,T.c') <> {}; let g be Morphism of T.c,T.c'; g in Hom(T.c,T.c') by A10,Def7; then g in rng hom(T,c,c') by A9; then consider f being set such that A11: f in dom hom(T,c,c') and A12: hom(T,c,c').f = g by FUNCT_1:def 5; A13: f in Hom(c,c') by A10,A11,FUNCT_2:def 1; thus Hom(c,c') <> {} by A11,FUNCT_2:def 1; reconsider f as Morphism of c,c' by A13,Def7; take f; thus T.f = g by A12,A13,Th131; end; theorem for T being Functor of C,D holds T is faithful iff for c,c' being Object of C holds hom(T,c,c') is one-to-one proof let T be Functor of C,D; thus T is faithful implies for c,c' being Object of C holds hom(T,c,c') is one-to-one proof assume A1: T is faithful; let c,c' be Object of C; A2: now assume Hom(T.c,T.c') = {}; then Hom(c,c') = {} by Th126; hence hom(T,c,c') is one-to-one by PARTFUN1:59; end; now assume A3: Hom(T.c,T.c') <> {}; now let f1,f2 be set; assume f1 in Hom(c,c') & f2 in Hom(c,c'); then A4: f1 is Morphism of c,c' & f2 is Morphism of c,c' & Hom(c,c') <> {} by Def7; then T.f1 = hom(T,c,c').f1 & T.f2 = hom(T,c,c').f2 by Th131; hence hom(T,c,c').f1 = hom(T,c,c').f2 implies f1 = f2 by A1,A4,Def24; end; hence hom(T,c,c') is one-to-one by A3,FUNCT_2:25; end; hence thesis by A2; end; assume A5: for c,c' being Object of C holds hom(T,c,c') is one-to-one; let c,c' be Object of C such that A6: Hom(c,c') <> {}; let f1,f2 be Morphism of c,c'; Hom(T.c,T.c') <> {} & f1 in Hom(c,c') & f2 in Hom(c,c') & hom(T,c,c') is one-to-one & T.f1 = hom(T,c,c').f1 & T.f2 = hom(T,c,c').f2 by A5,A6,Def7,Th126,Th131; hence thesis by FUNCT_2:25; end;