:: ALTCAT_2 semantic presentation begin theorem :: ALTCAT_2:1 for X1, X2, a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2] proof let X1, X2 be set ; ::_thesis: for a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2] let a1, a2 be set ; ::_thesis: [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2] A1: ( dom (X1 --> a1) = X1 & dom (X2 --> a2) = X2 ) by FUNCOP_1:13; then A2: dom ([:X1,X2:] --> [a1,a2]) = [:(dom (X1 --> a1)),(dom (X2 --> a2)):] by FUNCOP_1:13; now__::_thesis:_for_x,_y_being_set_st_x_in_dom_(X1_-->_a1)_&_y_in_dom_(X2_-->_a2)_holds_ ([:X1,X2:]_-->_[a1,a2])_._(x,y)_=_[((X1_-->_a1)_._x),((X2_-->_a2)_._y)] let x, y be set ; ::_thesis: ( x in dom (X1 --> a1) & y in dom (X2 --> a2) implies ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] ) assume A3: ( x in dom (X1 --> a1) & y in dom (X2 --> a2) ) ; ::_thesis: ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] then [x,y] in dom ([:X1,X2:] --> [a1,a2]) by A2, ZFMISC_1:87; then A4: [x,y] in [:X1,X2:] by FUNCOP_1:13; ( (X1 --> a1) . x = a1 & (X2 --> a2) . y = a2 ) by A1, A3, FUNCOP_1:7; hence ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] by A4, FUNCOP_1:7; ::_thesis: verum end; hence [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2] by A2, FUNCT_3:def_8; ::_thesis: verum end; registration let I be set ; cluster [[0]] I -> Function-yielding ; coherence [[0]] I is Function-yielding ; end; theorem :: ALTCAT_2:2 for f, g being Function holds ~ (g * f) = g * (~ f) proof let f, g be Function; ::_thesis: ~ (g * f) = g * (~ f) A1: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(g_*_(~_f))_implies_ex_y1,_z1_being_set_st_ (_x_=_[z1,y1]_&_[y1,z1]_in_dom_(g_*_f)_)_)_&_(_ex_y,_z_being_set_st_ (_x_=_[z,y]_&_[y,z]_in_dom_(g_*_f)_)_implies_x_in_dom_(g_*_(~_f))_)_) let x be set ; ::_thesis: ( ( x in dom (g * (~ f)) implies ex y1, z1 being set st ( x = [z1,y1] & [y1,z1] in dom (g * f) ) ) & ( ex y, z being set st ( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) ) ) hereby ::_thesis: ( ex y, z being set st ( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) ) assume A2: x in dom (g * (~ f)) ; ::_thesis: ex y1, z1 being set st ( x = [z1,y1] & [y1,z1] in dom (g * f) ) then x in dom (~ f) by FUNCT_1:11; then consider y1, z1 being set such that A3: x = [z1,y1] and A4: [y1,z1] in dom f by FUNCT_4:def_2; take y1 = y1; ::_thesis: ex z1 being set st ( x = [z1,y1] & [y1,z1] in dom (g * f) ) take z1 = z1; ::_thesis: ( x = [z1,y1] & [y1,z1] in dom (g * f) ) thus x = [z1,y1] by A3; ::_thesis: [y1,z1] in dom (g * f) (~ f) . (z1,y1) in dom g by A2, A3, FUNCT_1:11; then f . (y1,z1) in dom g by A4, FUNCT_4:def_2; hence [y1,z1] in dom (g * f) by A4, FUNCT_1:11; ::_thesis: verum end; given y, z being set such that A5: x = [z,y] and A6: [y,z] in dom (g * f) ; ::_thesis: x in dom (g * (~ f)) A7: [y,z] in dom f by A6, FUNCT_1:11; then A8: x in dom (~ f) by A5, FUNCT_4:def_2; f . (y,z) in dom g by A6, FUNCT_1:11; then (~ f) . (z,y) in dom g by A7, FUNCT_4:def_2; hence x in dom (g * (~ f)) by A5, A8, FUNCT_1:11; ::_thesis: verum end; now__::_thesis:_for_y,_z_being_set_st_[y,z]_in_dom_(g_*_f)_holds_ (g_*_(~_f))_._(z,y)_=_(g_*_f)_._(y,z) let y, z be set ; ::_thesis: ( [y,z] in dom (g * f) implies (g * (~ f)) . (z,y) = (g * f) . (y,z) ) assume A9: [y,z] in dom (g * f) ; ::_thesis: (g * (~ f)) . (z,y) = (g * f) . (y,z) then [y,z] in dom f by FUNCT_1:11; then A10: [z,y] in dom (~ f) by FUNCT_4:42; hence (g * (~ f)) . (z,y) = g . ((~ f) . (z,y)) by FUNCT_1:13 .= g . (f . (y,z)) by A10, FUNCT_4:43 .= (g * f) . (y,z) by A9, FUNCT_1:12 ; ::_thesis: verum end; hence ~ (g * f) = g * (~ f) by A1, FUNCT_4:def_2; ::_thesis: verum end; theorem :: ALTCAT_2:3 for f, g, h being Function holds ~ (f * [:g,h:]) = (~ f) * [:h,g:] proof let f, g, h be Function; ::_thesis: ~ (f * [:g,h:]) = (~ f) * [:h,g:] A1: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_((~_f)_*_[:h,g:])_implies_ex_z1,_y1_being_set_st_ (_x_=_[y1,z1]_&_[z1,y1]_in_dom_(f_*_[:g,h:])_)_)_&_(_ex_y,_z_being_set_st_ (_x_=_[z,y]_&_[y,z]_in_dom_(f_*_[:g,h:])_)_implies_x_in_dom_((~_f)_*_[:h,g:])_)_) let x be set ; ::_thesis: ( ( x in dom ((~ f) * [:h,g:]) implies ex z1, y1 being set st ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being set st ( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) ) hereby ::_thesis: ( ex y, z being set st ( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) assume A2: x in dom ((~ f) * [:h,g:]) ; ::_thesis: ex z1, y1 being set st ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) then x in dom [:h,g:] by FUNCT_1:11; then x in [:(dom h),(dom g):] by FUNCT_3:def_8; then consider y1, z1 being set such that A3: ( y1 in dom h & z1 in dom g ) and A4: x = [y1,z1] by ZFMISC_1:84; A5: ( [:h,g:] . (y1,z1) = [(h . y1),(g . z1)] & [:g,h:] . (z1,y1) = [(g . z1),(h . y1)] ) by A3, FUNCT_3:def_8; [:h,g:] . (y1,z1) in dom (~ f) by A2, A4, FUNCT_1:11; then A6: [:g,h:] . (z1,y1) in dom f by A5, FUNCT_4:42; take z1 = z1; ::_thesis: ex y1 being set st ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) take y1 = y1; ::_thesis: ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) thus x = [y1,z1] by A4; ::_thesis: [z1,y1] in dom (f * [:g,h:]) dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def_8; then [z1,y1] in dom [:g,h:] by A3, ZFMISC_1:87; hence [z1,y1] in dom (f * [:g,h:]) by A6, FUNCT_1:11; ::_thesis: verum end; given y, z being set such that A7: x = [z,y] and A8: [y,z] in dom (f * [:g,h:]) ; ::_thesis: x in dom ((~ f) * [:h,g:]) A9: [:g,h:] . (y,z) in dom f by A8, FUNCT_1:11; A10: dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def_8; [y,z] in dom [:g,h:] by A8, FUNCT_1:11; then A11: ( y in dom g & z in dom h ) by A10, ZFMISC_1:87; then ( [:g,h:] . (y,z) = [(g . y),(h . z)] & [:h,g:] . (z,y) = [(h . z),(g . y)] ) by FUNCT_3:def_8; then A12: [:h,g:] . x in dom (~ f) by A7, A9, FUNCT_4:42; dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def_8; then x in dom [:h,g:] by A7, A11, ZFMISC_1:87; hence x in dom ((~ f) * [:h,g:]) by A12, FUNCT_1:11; ::_thesis: verum end; now__::_thesis:_for_y,_z_being_set_st_[y,z]_in_dom_(f_*_[:g,h:])_holds_ ((~_f)_*_[:h,g:])_._(z,y)_=_(f_*_[:g,h:])_._(y,z) let y, z be set ; ::_thesis: ( [y,z] in dom (f * [:g,h:]) implies ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z) ) assume A13: [y,z] in dom (f * [:g,h:]) ; ::_thesis: ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z) then [y,z] in dom [:g,h:] by FUNCT_1:11; then [y,z] in [:(dom g),(dom h):] by FUNCT_3:def_8; then A14: ( y in dom g & z in dom h ) by ZFMISC_1:87; [:g,h:] . (y,z) in dom f by A13, FUNCT_1:11; then A15: [(g . y),(h . z)] in dom f by A14, FUNCT_3:def_8; [z,y] in [:(dom h),(dom g):] by A14, ZFMISC_1:87; then [z,y] in dom [:h,g:] by FUNCT_3:def_8; hence ((~ f) * [:h,g:]) . (z,y) = (~ f) . ([:h,g:] . (z,y)) by FUNCT_1:13 .= (~ f) . ((h . z),(g . y)) by A14, FUNCT_3:def_8 .= f . ((g . y),(h . z)) by A15, FUNCT_4:def_2 .= f . ([:g,h:] . (y,z)) by A14, FUNCT_3:def_8 .= (f * [:g,h:]) . (y,z) by A13, FUNCT_1:12 ; ::_thesis: verum end; hence ~ (f * [:g,h:]) = (~ f) * [:h,g:] by A1, FUNCT_4:def_2; ::_thesis: verum end; registration let f be Function-yielding Function; cluster ~ f -> Function-yielding ; coherence ~ f is Function-yielding proof let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (~ f) or (~ f) . x is set ) assume x in dom (~ f) ; ::_thesis: (~ f) . x is set then consider z, y being set such that A1: x = [y,z] and A2: [z,y] in dom f by FUNCT_4:def_2; f . (z,y) = (~ f) . (y,z) by A2, FUNCT_4:def_2; hence (~ f) . x is set by A1; ::_thesis: verum end; end; theorem :: ALTCAT_2:4 for I being set for A, B, C being ManySortedSet of I st A is_transformable_to B holds for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C proof let I be set ; ::_thesis: for A, B, C being ManySortedSet of I st A is_transformable_to B holds for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C let A, B, C be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C ) assume A1: A is_transformable_to B ; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C let G be ManySortedFunction of B,C; ::_thesis: G ** F is ManySortedFunction of A,C reconsider GF = G ** F as ManySortedFunction of I by MSSUBFAM:15; GF is ManySortedFunction of A,C proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or GF . i is Element of bool [:(A . i),(C . i):] ) assume A2: i in I ; ::_thesis: GF . i is Element of bool [:(A . i),(C . i):] then reconsider Gi = G . i as Function of (B . i),(C . i) by PBOOLE:def_15; reconsider Fi = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def_15; i in dom GF by A2, PARTFUN1:def_2; then A3: (G ** F) . i = Gi * Fi by PBOOLE:def_19; ( B . i = {} implies A . i = {} ) by A1, A2, PZFMISC1:def_3; hence GF . i is Element of bool [:(A . i),(C . i):] by A3, FUNCT_2:13; ::_thesis: verum end; hence G ** F is ManySortedFunction of A,C ; ::_thesis: verum end; registration let I be set ; let A be ManySortedSet of [:I,I:]; cluster ~ A -> [:I,I:] -defined ; coherence ~ A is [:I,I:] -defined ; end; registration let I be set ; let A be ManySortedSet of [:I,I:]; cluster ~ A -> [:I,I:] -defined total for [:I,I:] -defined Function; coherence for b1 being [:I,I:] -defined Function st b1 = ~ A holds b1 is total ; end; theorem :: ALTCAT_2:5 for I1 being set for I2 being non empty set for f being Function of I1,I2 for B, C being ManySortedSet of I2 for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f proof let I1 be set ; ::_thesis: for I2 being non empty set for f being Function of I1,I2 for B, C being ManySortedSet of I2 for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f let I2 be non empty set ; ::_thesis: for f being Function of I1,I2 for B, C being ManySortedSet of I2 for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f let f be Function of I1,I2; ::_thesis: for B, C being ManySortedSet of I2 for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f let B, C be ManySortedSet of I2; ::_thesis: for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f let G be ManySortedFunction of B,C; ::_thesis: G * f is ManySortedFunction of B * f,C * f let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I1 or (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] ) assume A1: i in I1 ; ::_thesis: (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] then A2: G . (f . i) is Function of (B . (f . i)),(C . (f . i)) by FUNCT_2:5, PBOOLE:def_15; A3: i in dom f by A1, FUNCT_2:def_1; then ( B . (f . i) = (B * f) . i & C . (f . i) = (C * f) . i ) by FUNCT_1:13; hence (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] by A3, A2, FUNCT_1:13; ::_thesis: verum end; definition let I be set ; let A, B be ManySortedSet of [:I,I:]; let F be ManySortedFunction of A,B; :: original: ~ redefine func ~ F -> ManySortedFunction of ~ A, ~ B; coherence ~ F is ManySortedFunction of ~ A, ~ B proof reconsider G = ~ F as ManySortedSet of [:I,I:] ; G is ManySortedFunction of ~ A, ~ B proof let ii be set ; :: according to PBOOLE:def_15 ::_thesis: ( not ii in [:I,I:] or G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] ) assume ii in [:I,I:] ; ::_thesis: G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] then consider i1, i2 being set such that A1: ( i1 in I & i2 in I ) and A2: ii = [i1,i2] by ZFMISC_1:84; A3: [i2,i1] in [:I,I:] by A1, ZFMISC_1:87; dom B = [:I,I:] by PARTFUN1:def_2; then A4: B . (i2,i1) = (~ B) . (i1,i2) by A3, FUNCT_4:def_2; dom A = [:I,I:] by PARTFUN1:def_2; then A5: A . (i2,i1) = (~ A) . (i1,i2) by A3, FUNCT_4:def_2; dom F = [:I,I:] by PARTFUN1:def_2; then F . (i2,i1) = G . (i1,i2) by A3, FUNCT_4:def_2; hence G . ii is Element of bool [:((~ A) . ii),((~ B) . ii):] by A2, A3, A5, A4, PBOOLE:def_15; ::_thesis: verum end; hence ~ F is ManySortedFunction of ~ A, ~ B ; ::_thesis: verum end; end; theorem :: ALTCAT_2:6 for I1, I2 being non empty set for M being ManySortedSet of [:I1,I2:] for o1 being Element of I1 for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2) proof let I1, I2 be non empty set ; ::_thesis: for M being ManySortedSet of [:I1,I2:] for o1 being Element of I1 for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2) let M be ManySortedSet of [:I1,I2:]; ::_thesis: for o1 being Element of I1 for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2) let o1 be Element of I1; ::_thesis: for o2 being Element of I2 holds (~ M) . (o2,o1) = M . (o1,o2) let o2 be Element of I2; ::_thesis: (~ M) . (o2,o1) = M . (o1,o2) [o1,o2] in [:I1,I2:] ; then [o1,o2] in dom M by PARTFUN1:def_2; hence (~ M) . (o2,o1) = M . (o1,o2) by FUNCT_4:def_2; ::_thesis: verum end; registration let I1 be set ; let f, g be ManySortedFunction of I1; clusterg ** f -> I1 -defined ; coherence g ** f is I1 -defined proof A1: ( dom f = I1 & dom g = I1 ) by PARTFUN1:def_2; dom (g ** f) = (dom g) /\ (dom f) by PBOOLE:def_19 .= I1 by A1 ; hence g ** f is I1 -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let I1 be set ; let f, g be ManySortedFunction of I1; clusterg ** f -> total ; coherence g ** f is total proof A1: ( dom f = I1 & dom g = I1 ) by PARTFUN1:def_2; dom (g ** f) = (dom g) /\ (dom f) by PBOOLE:def_19 .= I1 by A1 ; hence g ** f is total by PARTFUN1:def_2; ::_thesis: verum end; end; begin definition let f, g be Function; predf cc= g means :Def1: :: ALTCAT_2:def 1 ( dom f c= dom g & ( for i being set st i in dom f holds f . i c= g . i ) ); reflexivity for f being Function holds ( dom f c= dom f & ( for i being set st i in dom f holds f . i c= f . i ) ) ; end; :: deftheorem Def1 defines cc= ALTCAT_2:def_1_:_ for f, g being Function holds ( f cc= g iff ( dom f c= dom g & ( for i being set st i in dom f holds f . i c= g . i ) ) ); definition let I, J be set ; let A be ManySortedSet of I; let B be ManySortedSet of J; :: original: cc= redefine predA cc= B means :Def2: :: ALTCAT_2:def 2 ( I c= J & ( for i being set st i in I holds A . i c= B . i ) ); compatibility ( A cc= B iff ( I c= J & ( for i being set st i in I holds A . i c= B . i ) ) ) proof A1: dom A = I by PARTFUN1:def_2; dom B = J by PARTFUN1:def_2; hence ( A cc= B implies ( I c= J & ( for i being set st i in I holds A . i c= B . i ) ) ) by A1, Def1; ::_thesis: ( I c= J & ( for i being set st i in I holds A . i c= B . i ) implies A cc= B ) assume that A2: I c= J and A3: for i being set st i in I holds A . i c= B . i ; ::_thesis: A cc= B thus dom A c= dom B by A1, A2, PARTFUN1:def_2; :: according to ALTCAT_2:def_1 ::_thesis: for i being set st i in dom A holds A . i c= B . i let i be set ; ::_thesis: ( i in dom A implies A . i c= B . i ) assume i in dom A ; ::_thesis: A . i c= B . i hence A . i c= B . i by A1, A3; ::_thesis: verum end; end; :: deftheorem Def2 defines cc= ALTCAT_2:def_2_:_ for I, J being set for A being ManySortedSet of I for B being ManySortedSet of J holds ( A cc= B iff ( I c= J & ( for i being set st i in I holds A . i c= B . i ) ) ); theorem Th7: :: ALTCAT_2:7 for I, J being set for A being ManySortedSet of I for B being ManySortedSet of J st A cc= B & B cc= A holds A = B proof let I, J be set ; ::_thesis: for A being ManySortedSet of I for B being ManySortedSet of J st A cc= B & B cc= A holds A = B let A be ManySortedSet of I; ::_thesis: for B being ManySortedSet of J st A cc= B & B cc= A holds A = B let B be ManySortedSet of J; ::_thesis: ( A cc= B & B cc= A implies A = B ) assume that A1: A cc= B and A2: B cc= A ; ::_thesis: A = B A3: I c= J by A1, Def2; J c= I by A2, Def2; then I = J by A3, XBOOLE_0:def_10; then reconsider B9 = B as ManySortedSet of I ; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ A_._i_=_B9_._i let i be set ; ::_thesis: ( i in I implies A . i = B9 . i ) assume i in I ; ::_thesis: A . i = B9 . i then ( A . i c= B . i & B . i c= A . i ) by A1, A2, A3, Def2; hence A . i = B9 . i by XBOOLE_0:def_10; ::_thesis: verum end; hence A = B by PBOOLE:3; ::_thesis: verum end; theorem Th8: :: ALTCAT_2:8 for I, J, K being set for A being ManySortedSet of I for B being ManySortedSet of J for C being ManySortedSet of K st A cc= B & B cc= C holds A cc= C proof let I, J, K be set ; ::_thesis: for A being ManySortedSet of I for B being ManySortedSet of J for C being ManySortedSet of K st A cc= B & B cc= C holds A cc= C let A be ManySortedSet of I; ::_thesis: for B being ManySortedSet of J for C being ManySortedSet of K st A cc= B & B cc= C holds A cc= C let B be ManySortedSet of J; ::_thesis: for C being ManySortedSet of K st A cc= B & B cc= C holds A cc= C let C be ManySortedSet of K; ::_thesis: ( A cc= B & B cc= C implies A cc= C ) assume that A1: A cc= B and A2: B cc= C ; ::_thesis: A cc= C A3: I c= J by A1, Def2; J c= K by A2, Def2; hence I c= K by A3, XBOOLE_1:1; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in I holds A . i c= C . i let i be set ; ::_thesis: ( i in I implies A . i c= C . i ) assume A4: i in I ; ::_thesis: A . i c= C . i then A5: A . i c= B . i by A1, Def2; B . i c= C . i by A2, A3, A4, Def2; hence A . i c= C . i by A5, XBOOLE_1:1; ::_thesis: verum end; theorem :: ALTCAT_2:9 for I being set for A, B being ManySortedSet of I holds ( A cc= B iff A c= B ) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds ( A cc= B iff A c= B ) let A, B be ManySortedSet of I; ::_thesis: ( A cc= B iff A c= B ) thus ( A cc= B implies A c= B ) ::_thesis: ( A c= B implies A cc= B ) proof assume A1: A cc= B ; ::_thesis: A c= B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= B . i ) thus ( not i in I or A . i c= B . i ) by A1, Def2; ::_thesis: verum end; assume A2: A c= B ; ::_thesis: A cc= B thus I c= I ; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in I holds A . i c= B . i thus for i being set st i in I holds A . i c= B . i by A2, PBOOLE:def_2; ::_thesis: verum end; begin scheme :: ALTCAT_2:sch 1 OnSingletons{ F1() -> non empty set , F2( set ) -> set , P1[ set ] } : { [o,F2(o)] where o is Element of F1() : P1[o] } is Function proof set f = { [o,F2(o)] where o is Element of F1() : P1[o] } ; A1: { [o,F2(o)] where o is Element of F1() : P1[o] } is Function-like proof let x, y1, y2 be set ; :: according to FUNCT_1:def_1 ::_thesis: ( not [x,y1] in { [o,F2(o)] where o is Element of F1() : P1[o] } or not [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } or y1 = y2 ) assume [x,y1] in { [o,F2(o)] where o is Element of F1() : P1[o] } ; ::_thesis: ( not [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } or y1 = y2 ) then consider o1 being Element of F1() such that A2: [x,y1] = [o1,F2(o1)] and P1[o1] ; A3: o1 = x by A2, XTUPLE_0:1; assume [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } ; ::_thesis: y1 = y2 then consider o2 being Element of F1() such that A4: [x,y2] = [o2,F2(o2)] and P1[o2] ; o2 = x by A4, XTUPLE_0:1; hence y1 = y2 by A2, A4, A3, XTUPLE_0:1; ::_thesis: verum end; { [o,F2(o)] where o is Element of F1() : P1[o] } is Relation-like proof let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in { [o,F2(o)] where o is Element of F1() : P1[o] } or ex b1, b2 being set st x = [b1,b2] ) assume x in { [o,F2(o)] where o is Element of F1() : P1[o] } ; ::_thesis: ex b1, b2 being set st x = [b1,b2] then consider o being Element of F1() such that A5: x = [o,F2(o)] and P1[o] ; take o ; ::_thesis: ex b1 being set st x = [o,b1] take F2(o) ; ::_thesis: x = [o,F2(o)] thus x = [o,F2(o)] by A5; ::_thesis: verum end; hence { [o,F2(o)] where o is Element of F1() : P1[o] } is Function by A1; ::_thesis: verum end; scheme :: ALTCAT_2:sch 2 DomOnSingletons{ F1() -> non empty set , F2() -> Function, F3( set ) -> set , P1[ set ] } : dom F2() = { o where o is Element of F1() : P1[o] } provided A1: F2() = { [o,F3(o)] where o is Element of F1() : P1[o] } proof set A = { o where o is Element of F1() : P1[o] } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__o_where_o_is_Element_of_F1()_:_P1[o]__}__implies_ex_y_being_set_st_[x,y]_in_F2()_)_&_(_ex_y_being_set_st_[x,y]_in_F2()_implies_x_in__{__o_where_o_is_Element_of_F1()_:_P1[o]__}__)_) let x be set ; ::_thesis: ( ( x in { o where o is Element of F1() : P1[o] } implies ex y being set st [x,y] in F2() ) & ( ex y being set st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } ) ) hereby ::_thesis: ( ex y being set st [x,y] in F2() implies x in { o where o is Element of F1() : P1[o] } ) assume x in { o where o is Element of F1() : P1[o] } ; ::_thesis: ex y being set st [x,y] in F2() then consider o being Element of F1() such that A2: ( x = o & P1[o] ) ; take y = F3(o); ::_thesis: [x,y] in F2() thus [x,y] in F2() by A1, A2; ::_thesis: verum end; given y being set such that A3: [x,y] in F2() ; ::_thesis: x in { o where o is Element of F1() : P1[o] } consider o being Element of F1() such that A4: [x,y] = [o,F3(o)] and A5: P1[o] by A1, A3; x = o by A4, XTUPLE_0:1; hence x in { o where o is Element of F1() : P1[o] } by A5; ::_thesis: verum end; hence dom F2() = { o where o is Element of F1() : P1[o] } by XTUPLE_0:def_12; ::_thesis: verum end; scheme :: ALTCAT_2:sch 3 ValOnSingletons{ F1() -> non empty set , F2() -> Function, F3() -> Element of F1(), F4( set ) -> set , P1[ set ] } : F2() . F3() = F4(F3()) provided A1: F2() = { [o,F4(o)] where o is Element of F1() : P1[o] } and A2: P1[F3()] proof A3: F2() = { [o,F4(o)] where o is Element of F1() : P1[o] } by A1; dom F2() = { o where o is Element of F1() : P1[o] } from ALTCAT_2:sch_2(A3); then A4: F3() in dom F2() by A2; [F3(),F4(F3())] in { [o,F4(o)] where o is Element of F1() : P1[o] } by A2; hence F2() . F3() = F4(F3()) by A1, A4, FUNCT_1:def_2; ::_thesis: verum end; begin theorem Th10: :: ALTCAT_2:10 for C being Category for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C proof let C be Category; ::_thesis: for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C let i, j, k be Object of C; ::_thesis: [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in [:(Hom (j,k)),(Hom (i,j)):] or e in dom the Comp of C ) assume A1: e in [:(Hom (j,k)),(Hom (i,j)):] ; ::_thesis: e in dom the Comp of C then reconsider y = e `1 , x = e `2 as Morphism of C by MCART_1:10; A2: e `2 in Hom (i,j) by A1, MCART_1:10; A3: e = [y,x] by A1, MCART_1:21; e `1 in Hom (j,k) by A1, MCART_1:10; then dom y = j by CAT_1:1 .= cod x by A2, CAT_1:1 ; hence e in dom the Comp of C by A3, CAT_1:15; ::_thesis: verum end; theorem Th11: :: ALTCAT_2:11 for C being Category for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) proof let C be Category; ::_thesis: for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) let i, j, k be Object of C; ::_thesis: the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] or e in Hom (i,k) ) assume e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] ; ::_thesis: e in Hom (i,k) then consider x being set such that A1: x in dom the Comp of C and A2: x in [:(Hom (j,k)),(Hom (i,j)):] and A3: e = the Comp of C . x by FUNCT_1:def_6; reconsider y = x `1 , z = x `2 as Morphism of C by A2, MCART_1:10; A4: ( x = [y,z] & e = the Comp of C . (y,z) ) by A2, A3, MCART_1:21; A5: x `2 in Hom (i,j) by A2, MCART_1:10; then A6: z is Morphism of i,j by CAT_1:def_5; A7: x `1 in Hom (j,k) by A2, MCART_1:10; then y is Morphism of j,k by CAT_1:def_5; then y (*) z in Hom (i,k) by A7, A5, A6, CAT_1:23; hence e in Hom (i,k) by A1, A4, CAT_1:def_1; ::_thesis: verum end; definition let C be non empty non void CatStr ; func the_hom_sets_of C -> ManySortedSet of [: the carrier of C, the carrier of C:] means :Def3: :: ALTCAT_2:def 3 for i, j being Object of C holds it . (i,j) = Hom (i,j); existence ex b1 being ManySortedSet of [: the carrier of C, the carrier of C:] st for i, j being Object of C holds b1 . (i,j) = Hom (i,j) proof deffunc H1( Object of C, Object of C) -> Element of bool the carrier' of C = Hom (\$1,\$2); thus ex M being ManySortedSet of [: the carrier of C, the carrier of C:] st for i, j being Object of C holds M . (i,j) = H1(i,j) from ALTCAT_1:sch_2(); ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of [: the carrier of C, the carrier of C:] st ( for i, j being Object of C holds b1 . (i,j) = Hom (i,j) ) & ( for i, j being Object of C holds b2 . (i,j) = Hom (i,j) ) holds b1 = b2 proof let M1, M2 be ManySortedSet of [: the carrier of C, the carrier of C:]; ::_thesis: ( ( for i, j being Object of C holds M1 . (i,j) = Hom (i,j) ) & ( for i, j being Object of C holds M2 . (i,j) = Hom (i,j) ) implies M1 = M2 ) assume that A1: for i, j being Object of C holds M1 . (i,j) = Hom (i,j) and A2: for i, j being Object of C holds M2 . (i,j) = Hom (i,j) ; ::_thesis: M1 = M2 now__::_thesis:_for_i,_j_being_Object_of_C_holds_M1_._(i,j)_=_M2_._(i,j) let i, j be Object of C; ::_thesis: M1 . (i,j) = M2 . (i,j) thus M1 . (i,j) = Hom (i,j) by A1 .= M2 . (i,j) by A2 ; ::_thesis: verum end; hence M1 = M2 by ALTCAT_1:7; ::_thesis: verum end; end; :: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def_3_:_ for C being non empty non void CatStr for b2 being ManySortedSet of [: the carrier of C, the carrier of C:] holds ( b2 = the_hom_sets_of C iff for i, j being Object of C holds b2 . (i,j) = Hom (i,j) ); theorem Th12: :: ALTCAT_2:12 for C being Category for i being Object of C holds id i in (the_hom_sets_of C) . (i,i) proof let C be Category; ::_thesis: for i being Object of C holds id i in (the_hom_sets_of C) . (i,i) let i be Object of C; ::_thesis: id i in (the_hom_sets_of C) . (i,i) id i in Hom (i,i) by CAT_1:27; hence id i in (the_hom_sets_of C) . (i,i) by Def3; ::_thesis: verum end; definition let C be Category; func the_comps_of C -> BinComp of (the_hom_sets_of C) means :Def4: :: ALTCAT_2:def 4 for i, j, k being Object of C holds it . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]; existence ex b1 being BinComp of (the_hom_sets_of C) st for i, j, k being Object of C holds b1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] proof deffunc H1( set ) -> Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] = the Comp of C | [:((the_hom_sets_of C) . (((\$1 `1) `2),(\$1 `2))),((the_hom_sets_of C) . (((\$1 `1) `1),((\$1 `1) `2))):]; set Ob3 = [: the carrier of C, the carrier of C, the carrier of C:]; set G = the_hom_sets_of C; consider o being Function such that A1: dom o = [: the carrier of C, the carrier of C, the carrier of C:] and A2: for e being set st e in [: the carrier of C, the carrier of C, the carrier of C:] holds o . e = H1(e) from FUNCT_1:sch_3(); reconsider o = o as ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] by A1, PARTFUN1:def_2, RELAT_1:def_18; now__::_thesis:_for_e_being_set_st_e_in_dom_o_holds_ o_._e_is_Function let e be set ; ::_thesis: ( e in dom o implies o . e is Function ) assume e in dom o ; ::_thesis: o . e is Function then o . e = the Comp of C | [:((the_hom_sets_of C) . (((e `1) `2),(e `2))),((the_hom_sets_of C) . (((e `1) `1),((e `1) `2))):] by A1, A2; hence o . e is Function ; ::_thesis: verum end; then reconsider o = o as ManySortedFunction of [: the carrier of C, the carrier of C, the carrier of C:] by FUNCOP_1:def_6; now__::_thesis:_for_e_being_set_st_e_in_[:_the_carrier_of_C,_the_carrier_of_C,_the_carrier_of_C:]_holds_ o_._e_is_Function_of_({|(the_hom_sets_of_C),(the_hom_sets_of_C)|}_._e),({|(the_hom_sets_of_C)|}_._e) let e be set ; ::_thesis: ( e in [: the carrier of C, the carrier of C, the carrier of C:] implies o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) ) reconsider f = o . e as Function ; assume A3: e in [: the carrier of C, the carrier of C, the carrier of C:] ; ::_thesis: o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) then consider i, j, k being Object of C such that A4: e = [i,j,k] by DOMAIN_1:3; reconsider e9 = e as Element of [: the carrier of C, the carrier of C, the carrier of C:] by A3; A5: ([i,j,k] `1) `2 = e9 `2_3 by A4 .= j by A4, MCART_1:def_6 ; A6: [i,j,k] `2 = e9 `3_3 by A4 .= k by A4, MCART_1:def_7 ; ([i,j,k] `1) `1 = e9 `1_3 by A4 .= i by A4, MCART_1:def_5 ; then A7: f = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A2, A4, A5, A6; A8: ( (the_hom_sets_of C) . (i,j) = Hom (i,j) & (the_hom_sets_of C) . (j,k) = Hom (j,k) ) by Def3; A9: {|(the_hom_sets_of C)|} . e = {|(the_hom_sets_of C)|} . (i,j,k) by A4, MULTOP_1:def_1 .= (the_hom_sets_of C) . (i,k) by ALTCAT_1:def_3 .= Hom (i,k) by Def3 ; A10: {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . (i,j,k) by A4, MULTOP_1:def_1 .= [:(Hom (j,k)),(Hom (i,j)):] by A8, ALTCAT_1:def_4 ; the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) by Th11; then A11: rng f c= {|(the_hom_sets_of C)|} . e by A8, A7, A9, RELAT_1:115; [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C by Th10; then dom f = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e by A8, A7, A10, RELAT_1:62; hence o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) by A11, FUNCT_2:2; ::_thesis: verum end; then reconsider o = o as BinComp of (the_hom_sets_of C) by PBOOLE:def_15; take o ; ::_thesis: for i, j, k being Object of C holds o . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] let i, j, k be Object of C; ::_thesis: o . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] reconsider e = [i,j,k] as Element of [: the carrier of C, the carrier of C, the carrier of C:] ; A12: ([i,j,k] `1) `1 = e `1_3 .= i by MCART_1:def_5 ; A13: ([i,j,k] `1) `2 = e `2_3 .= j by MCART_1:def_6 ; A14: [i,j,k] `2 = e `3_3 .= k by MCART_1:def_7 ; thus o . (i,j,k) = o . [i,j,k] by MULTOP_1:def_1 .= the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A2, A12, A13, A14 ; ::_thesis: verum end; uniqueness for b1, b2 being BinComp of (the_hom_sets_of C) st ( for i, j, k being Object of C holds b1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds b2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) holds b1 = b2 proof let o1, o2 be BinComp of (the_hom_sets_of C); ::_thesis: ( ( for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) implies o1 = o2 ) assume that A15: for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] and A16: for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ; ::_thesis: o1 = o2 now__::_thesis:_for_a_being_set_st_a_in_[:_the_carrier_of_C,_the_carrier_of_C,_the_carrier_of_C:]_holds_ o1_._a_=_o2_._a let a be set ; ::_thesis: ( a in [: the carrier of C, the carrier of C, the carrier of C:] implies o1 . a = o2 . a ) assume a in [: the carrier of C, the carrier of C, the carrier of C:] ; ::_thesis: o1 . a = o2 . a then consider i, j, k being Object of C such that A17: a = [i,j,k] by DOMAIN_1:3; thus o1 . a = o1 . (i,j,k) by A17, MULTOP_1:def_1 .= the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A15 .= o2 . (i,j,k) by A16 .= o2 . a by A17, MULTOP_1:def_1 ; ::_thesis: verum end; hence o1 = o2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def4 defines the_comps_of ALTCAT_2:def_4_:_ for C being Category for b2 being BinComp of (the_hom_sets_of C) holds ( b2 = the_comps_of C iff for i, j, k being Object of C holds b2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ); theorem Th13: :: ALTCAT_2:13 for C being Category for i, j, k being Object of C st Hom (i,j) <> {} & Hom (j,k) <> {} holds for f being Morphism of i,j for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f proof let C be Category; ::_thesis: for i, j, k being Object of C st Hom (i,j) <> {} & Hom (j,k) <> {} holds for f being Morphism of i,j for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f let i, j, k be Object of C; ::_thesis: ( Hom (i,j) <> {} & Hom (j,k) <> {} implies for f being Morphism of i,j for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f ) assume that A1: Hom (i,j) <> {} and A2: Hom (j,k) <> {} ; ::_thesis: for f being Morphism of i,j for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f let f be Morphism of i,j; ::_thesis: for g being Morphism of j,k holds ((the_comps_of C) . (i,j,k)) . (g,f) = g * f let g be Morphism of j,k; ::_thesis: ((the_comps_of C) . (i,j,k)) . (g,f) = g * f A3: g in Hom (j,k) by A2, CAT_1:def_5; then A4: g in (the_hom_sets_of C) . (j,k) by Def3; A5: f in Hom (i,j) by A1, CAT_1:def_5; then f in (the_hom_sets_of C) . (i,j) by Def3; then A6: [g,f] in [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A4, ZFMISC_1:87; A7: dom g = j by A3, CAT_1:1 .= cod f by A5, CAT_1:1 ; thus ((the_comps_of C) . (i,j,k)) . (g,f) = ( the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):]) . [g,f] by Def4 .= the Comp of C . (g,f) by A6, FUNCT_1:49 .= g (*) f by A7, CAT_1:16 .= g * f by A1, A2, CAT_1:def_13 ; ::_thesis: verum end; theorem Th14: :: ALTCAT_2:14 for C being Category holds the_comps_of C is associative proof let C be Category; ::_thesis: the_comps_of C is associative let i, j, k, l be Object of C; :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds ( not b1 in (the_hom_sets_of C) . (i,j) or not b2 in (the_hom_sets_of C) . (j,k) or not b3 in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (b3,(((the_comps_of C) . (i,j,k)) . (b2,b1))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (b3,b2)),b1) ) let f, g, h be set ; ::_thesis: ( not f in (the_hom_sets_of C) . (i,j) or not g in (the_hom_sets_of C) . (j,k) or not h in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) ) assume f in (the_hom_sets_of C) . (i,j) ; ::_thesis: ( not g in (the_hom_sets_of C) . (j,k) or not h in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) ) then A1: f in Hom (i,j) by Def3; then reconsider f9 = f as Morphism of i,j by CAT_1:def_5; assume g in (the_hom_sets_of C) . (j,k) ; ::_thesis: ( not h in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) ) then A2: g in Hom (j,k) by Def3; then reconsider g9 = g as Morphism of j,k by CAT_1:def_5; assume h in (the_hom_sets_of C) . (k,l) ; ::_thesis: ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) then A3: h in Hom (k,l) by Def3; then reconsider h9 = h as Morphism of k,l by CAT_1:def_5; A4: ( Hom (j,l) <> {} & ((the_comps_of C) . (j,k,l)) . (h,g) = h9 * g9 ) by A2, A3, Th13, CAT_1:24; ( Hom (i,k) <> {} & ((the_comps_of C) . (i,j,k)) . (g,f) = g9 * f9 ) by A1, A2, Th13, CAT_1:24; hence ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = h9 * (g9 * f9) by A3, Th13 .= (h9 * g9) * f9 by A1, A2, A3, CAT_1:25 .= ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) by A1, A4, Th13 ; ::_thesis: verum end; theorem Th15: :: ALTCAT_2:15 for C being Category holds ( the_comps_of C is with_left_units & the_comps_of C is with_right_units ) proof let C be Category; ::_thesis: ( the_comps_of C is with_left_units & the_comps_of C is with_right_units ) thus the_comps_of C is with_left_units ::_thesis: the_comps_of C is with_right_units proof let i be Object of C; :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st ( b1 in (the_hom_sets_of C) . (i,i) & ( for b2 being Element of the carrier of C for b3 being set holds ( not b3 in (the_hom_sets_of C) . (b2,i) or ((the_comps_of C) . (b2,i,i)) . (b1,b3) = b3 ) ) ) take id i ; ::_thesis: ( id i in (the_hom_sets_of C) . (i,i) & ( for b1 being Element of the carrier of C for b2 being set holds ( not b2 in (the_hom_sets_of C) . (b1,i) or ((the_comps_of C) . (b1,i,i)) . ((id i),b2) = b2 ) ) ) thus id i in (the_hom_sets_of C) . (i,i) by Th12; ::_thesis: for b1 being Element of the carrier of C for b2 being set holds ( not b2 in (the_hom_sets_of C) . (b1,i) or ((the_comps_of C) . (b1,i,i)) . ((id i),b2) = b2 ) let j be Object of C; ::_thesis: for b1 being set holds ( not b1 in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,i,i)) . ((id i),b1) = b1 ) let f be set ; ::_thesis: ( not f in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,i,i)) . ((id i),f) = f ) assume f in (the_hom_sets_of C) . (j,i) ; ::_thesis: ((the_comps_of C) . (j,i,i)) . ((id i),f) = f then A1: f in Hom (j,i) by Def3; then reconsider m = f as Morphism of j,i by CAT_1:def_5; Hom (i,i) <> {} ; hence ((the_comps_of C) . (j,i,i)) . ((id i),f) = (id i) * m by A1, Th13 .= f by A1, CAT_1:28 ; ::_thesis: verum end; let j be Object of C; :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st ( b1 in (the_hom_sets_of C) . (j,j) & ( for b2 being Element of the carrier of C for b3 being set holds ( not b3 in (the_hom_sets_of C) . (j,b2) or ((the_comps_of C) . (j,j,b2)) . (b3,b1) = b3 ) ) ) take id j ; ::_thesis: ( id j in (the_hom_sets_of C) . (j,j) & ( for b1 being Element of the carrier of C for b2 being set holds ( not b2 in (the_hom_sets_of C) . (j,b1) or ((the_comps_of C) . (j,j,b1)) . (b2,(id j)) = b2 ) ) ) thus id j in (the_hom_sets_of C) . (j,j) by Th12; ::_thesis: for b1 being Element of the carrier of C for b2 being set holds ( not b2 in (the_hom_sets_of C) . (j,b1) or ((the_comps_of C) . (j,j,b1)) . (b2,(id j)) = b2 ) let i be Object of C; ::_thesis: for b1 being set holds ( not b1 in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,j,i)) . (b1,(id j)) = b1 ) let f be set ; ::_thesis: ( not f in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,j,i)) . (f,(id j)) = f ) assume f in (the_hom_sets_of C) . (j,i) ; ::_thesis: ((the_comps_of C) . (j,j,i)) . (f,(id j)) = f then A2: f in Hom (j,i) by Def3; then reconsider m = f as Morphism of j,i by CAT_1:def_5; Hom (j,j) <> {} ; hence ((the_comps_of C) . (j,j,i)) . (f,(id j)) = m * (id j) by A2, Th13 .= f by A2, CAT_1:29 ; ::_thesis: verum end; begin definition let C be Category; func Alter C -> non empty strict AltCatStr equals :: ALTCAT_2:def 5 AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #); correctness coherence AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #) is non empty strict AltCatStr ; ; end; :: deftheorem defines Alter ALTCAT_2:def_5_:_ for C being Category holds Alter C = AltCatStr(# the carrier of C,(the_hom_sets_of C),(the_comps_of C) #); theorem Th16: :: ALTCAT_2:16 for C being Category holds Alter C is associative proof let C be Category; ::_thesis: Alter C is associative thus the Comp of (Alter C) is associative by Th14; :: according to ALTCAT_1:def_15 ::_thesis: verum end; theorem Th17: :: ALTCAT_2:17 for C being Category holds Alter C is with_units proof let C be Category; ::_thesis: Alter C is with_units thus ( the Comp of (Alter C) is with_left_units & the Comp of (Alter C) is with_right_units ) by Th15; :: according to ALTCAT_1:def_16 ::_thesis: verum end; theorem Th18: :: ALTCAT_2:18 for C being Category holds Alter C is transitive proof let C be Category; ::_thesis: Alter C is transitive let o1, o2, o3 be object of (Alter C); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: not <^o1,o3^> = {} reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C ; A2: <^o1,o3^> = Hom (x1,x3) by Def3; ( <^o1,o2^> = Hom (x1,x2) & <^o2,o3^> = Hom (x2,x3) ) by Def3; hence not <^o1,o3^> = {} by A1, A2, CAT_1:24; ::_thesis: verum end; registration let C be Category; cluster Alter C -> non empty transitive strict associative with_units ; coherence ( Alter C is transitive & Alter C is associative & Alter C is with_units ) by Th16, Th17, Th18; end; begin registration cluster non empty strict for AltGraph ; existence ex b1 being AltGraph st ( not b1 is empty & b1 is strict ) proof set M = the ManySortedSet of [:1,1:]; take A = AltGraph(# 1, the ManySortedSet of [:1,1:] #); ::_thesis: ( not A is empty & A is strict ) thus not the carrier of A is empty ; :: according to STRUCT_0:def_1 ::_thesis: A is strict thus A is strict ; ::_thesis: verum end; end; definition let C be AltGraph ; attrC is reflexive means :Def6: :: ALTCAT_2:def 6 for x being set st x in the carrier of C holds the Arrows of C . (x,x) <> {} ; end; :: deftheorem Def6 defines reflexive ALTCAT_2:def_6_:_ for C being AltGraph holds ( C is reflexive iff for x being set st x in the carrier of C holds the Arrows of C . (x,x) <> {} ); definition let C be non empty AltGraph ; redefine attr C is reflexive means :: ALTCAT_2:def 7 for o being object of C holds <^o,o^> <> {} ; compatibility ( C is reflexive iff for o being object of C holds <^o,o^> <> {} ) proof thus ( C is reflexive implies for o being object of C holds <^o,o^> <> {} ) by Def6; ::_thesis: ( ( for o being object of C holds <^o,o^> <> {} ) implies C is reflexive ) assume A1: for o being object of C holds <^o,o^> <> {} ; ::_thesis: C is reflexive let x be set ; :: according to ALTCAT_2:def_6 ::_thesis: ( x in the carrier of C implies the Arrows of C . (x,x) <> {} ) assume x in the carrier of C ; ::_thesis: the Arrows of C . (x,x) <> {} then reconsider o = x as object of C ; the Arrows of C . (x,x) = <^o,o^> ; hence the Arrows of C . (x,x) <> {} by A1; ::_thesis: verum end; end; :: deftheorem defines reflexive ALTCAT_2:def_7_:_ for C being non empty AltGraph holds ( C is reflexive iff for o being object of C holds <^o,o^> <> {} ); definition let C be non empty transitive AltCatStr ; redefine attr C is associative means :Def8: :: ALTCAT_2:def 8 for o1, o2, o3, o4 being object of C for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f); compatibility ( C is associative iff for o1, o2, o3, o4 being object of C for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) ) proof thus ( C is associative implies for o1, o2, o3, o4 being object of C for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) ) by ALTCAT_1:21; ::_thesis: ( ( for o1, o2, o3, o4 being object of C for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) ) implies C is associative ) assume A1: for o1, o2, o3, o4 being object of C for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) ; ::_thesis: C is associative let i, j, k, l be Element of C; :: according to ALTCAT_1:def_5,ALTCAT_1:def_15 ::_thesis: for b1, b2, b3 being set holds ( not b1 in the Arrows of C . (i,j) or not b2 in the Arrows of C . (j,k) or not b3 in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (b3,(( the Comp of C . (i,j,k)) . (b2,b1))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (b3,b2)),b1) ) reconsider o1 = i, o2 = j, o3 = k, o4 = l as object of C ; let f, g, h be set ; ::_thesis: ( not f in the Arrows of C . (i,j) or not g in the Arrows of C . (j,k) or not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) ) assume A2: f in the Arrows of C . (i,j) ; ::_thesis: ( not g in the Arrows of C . (j,k) or not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) ) then reconsider ff = f as Morphism of o1,o2 ; assume A3: g in the Arrows of C . (j,k) ; ::_thesis: ( not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) ) then A4: g in <^o2,o3^> ; f in <^o1,o2^> by A2; then A5: <^o1,o3^> <> {} by A4, ALTCAT_1:def_2; reconsider gg = g as Morphism of o2,o3 by A3; assume A6: h in the Arrows of C . (k,l) ; ::_thesis: ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) then reconsider hh = h as Morphism of o3,o4 ; A7: ( the Comp of C . (j,k,l)) . (h,g) = hh * gg by A3, A6, ALTCAT_1:def_8; h in <^o3,o4^> by A6; then A8: <^o2,o4^> <> {} by A4, ALTCAT_1:def_2; ( the Comp of C . (i,j,k)) . (g,f) = gg * ff by A2, A3, ALTCAT_1:def_8; hence ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = hh * (gg * ff) by A6, A5, ALTCAT_1:def_8 .= (hh * gg) * ff by A1, A2, A3, A6 .= ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) by A2, A8, A7, ALTCAT_1:def_8 ; ::_thesis: verum end; end; :: deftheorem Def8 defines associative ALTCAT_2:def_8_:_ for C being non empty transitive AltCatStr holds ( C is associative iff for o1, o2, o3, o4 being object of C for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) ); definition let C be non empty AltCatStr ; redefine attr C is with_units means :: ALTCAT_2:def 9 for o being object of C holds ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ); compatibility ( C is with_units iff for o being object of C holds ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ) proof hereby ::_thesis: ( ( for o being object of C holds ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ) implies C is with_units ) assume A1: C is with_units ; ::_thesis: for o being object of C holds ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) then reconsider C9 = C as non empty with_units AltCatStr ; let o be object of C; ::_thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) thus <^o,o^> <> {} by A1, ALTCAT_1:18; ::_thesis: ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) reconsider p = o as object of C9 ; reconsider i = idm p as Morphism of o,o ; take i = i; ::_thesis: for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) let o9 be object of C; ::_thesis: for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) let m9 be Morphism of o9,o; ::_thesis: for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) let m99 be Morphism of o,o9; ::_thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) thus ( <^o9,o^> <> {} implies i * m9 = m9 ) by ALTCAT_1:20; ::_thesis: ( <^o,o9^> <> {} implies m99 * i = m99 ) thus ( <^o,o9^> <> {} implies m99 * i = m99 ) by ALTCAT_1:def_17; ::_thesis: verum end; assume A2: for o being object of C holds ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ; ::_thesis: C is with_units hereby :: according to ALTCAT_1:def_7,ALTCAT_1:def_16 ::_thesis: the Comp of C is with_right_units let j be Element of C; ::_thesis: ex e being set st ( e in the Arrows of C . (j,j) & ( for i being Element of C for f being set st f in the Arrows of C . (i,j) holds ( the Comp of C . (i,j,j)) . (e,f) = f ) ) reconsider o = j as object of C ; consider m being Morphism of o,o such that A3: for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies m * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * m = m99 ) ) by A2; reconsider e = m as set ; take e = e; ::_thesis: ( e in the Arrows of C . (j,j) & ( for i being Element of C for f being set st f in the Arrows of C . (i,j) holds ( the Comp of C . (i,j,j)) . (e,f) = f ) ) A4: <^o,o^> <> {} by A2; hence e in the Arrows of C . (j,j) ; ::_thesis: for i being Element of C for f being set st f in the Arrows of C . (i,j) holds ( the Comp of C . (i,j,j)) . (e,f) = f let i be Element of C; ::_thesis: for f being set st f in the Arrows of C . (i,j) holds ( the Comp of C . (i,j,j)) . (e,f) = f let f be set ; ::_thesis: ( f in the Arrows of C . (i,j) implies ( the Comp of C . (i,j,j)) . (e,f) = f ) assume A5: f in the Arrows of C . (i,j) ; ::_thesis: ( the Comp of C . (i,j,j)) . (e,f) = f reconsider o9 = i as object of C ; reconsider m9 = f as Morphism of o9,o by A5; thus ( the Comp of C . (i,j,j)) . (e,f) = m * m9 by A4, A5, ALTCAT_1:def_8 .= f by A3, A5 ; ::_thesis: verum end; let i be Element of C; :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st ( b1 in the Arrows of C . (i,i) & ( for b2 being Element of the carrier of C for b3 being set holds ( not b3 in the Arrows of C . (i,b2) or ( the Comp of C . (i,i,b2)) . (b3,b1) = b3 ) ) ) reconsider o = i as object of C ; consider m being Morphism of o,o such that A6: for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies m * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * m = m99 ) ) by A2; take e = m; ::_thesis: ( e in the Arrows of C . (i,i) & ( for b1 being Element of the carrier of C for b2 being set holds ( not b2 in the Arrows of C . (i,b1) or ( the Comp of C . (i,i,b1)) . (b2,e) = b2 ) ) ) A7: <^o,o^> <> {} by A2; hence e in the Arrows of C . (i,i) ; ::_thesis: for b1 being Element of the carrier of C for b2 being set holds ( not b2 in the Arrows of C . (i,b1) or ( the Comp of C . (i,i,b1)) . (b2,e) = b2 ) let j be Element of C; ::_thesis: for b1 being set holds ( not b1 in the Arrows of C . (i,j) or ( the Comp of C . (i,i,j)) . (b1,e) = b1 ) let f be set ; ::_thesis: ( not f in the Arrows of C . (i,j) or ( the Comp of C . (i,i,j)) . (f,e) = f ) assume A8: f in the Arrows of C . (i,j) ; ::_thesis: ( the Comp of C . (i,i,j)) . (f,e) = f reconsider o9 = j as object of C ; reconsider m9 = f as Morphism of o,o9 by A8; thus ( the Comp of C . (i,i,j)) . (f,e) = m9 * m by A7, A8, ALTCAT_1:def_8 .= f by A6, A8 ; ::_thesis: verum end; end; :: deftheorem defines with_units ALTCAT_2:def_9_:_ for C being non empty AltCatStr holds ( C is with_units iff for o being object of C holds ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of C for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ); registration cluster non empty with_units -> non empty reflexive for AltCatStr ; coherence for b1 being non empty AltCatStr st b1 is with_units holds b1 is reflexive proof let C be non empty AltCatStr ; ::_thesis: ( C is with_units implies C is reflexive ) assume A1: C is with_units ; ::_thesis: C is reflexive let o be object of C; :: according to ALTCAT_2:def_7 ::_thesis: <^o,o^> <> {} thus <^o,o^> <> {} by A1, ALTCAT_1:18; ::_thesis: verum end; end; registration cluster non empty reflexive for AltGraph ; existence ex b1 being AltGraph st ( not b1 is empty & b1 is reflexive ) proof set C = the non empty with_units AltCatStr ; take the non empty with_units AltCatStr ; ::_thesis: ( not the non empty with_units AltCatStr is empty & the non empty with_units AltCatStr is reflexive ) thus ( not the non empty with_units AltCatStr is empty & the non empty with_units AltCatStr is reflexive ) ; ::_thesis: verum end; end; registration cluster non empty reflexive for AltCatStr ; existence ex b1 being AltCatStr st ( not b1 is empty & b1 is reflexive ) proof set C = the category; take the category ; ::_thesis: ( not the category is empty & the category is reflexive ) thus ( not the category is empty & the category is reflexive ) ; ::_thesis: verum end; end; begin Lm1: for E1, E2 being strict AltCatStr st the carrier of E1 is empty & the carrier of E2 is empty holds E1 = E2 proof let E1, E2 be strict AltCatStr ; ::_thesis: ( the carrier of E1 is empty & the carrier of E2 is empty implies E1 = E2 ) set C1 = the carrier of E1; set C2 = the carrier of E2; assume that A1: the carrier of E1 is empty and A2: the carrier of E2 is empty ; ::_thesis: E1 = E2 A3: [: the carrier of E2, the carrier of E2, the carrier of E2:] = {} by A2, MCART_1:31; [: the carrier of E1, the carrier of E1, the carrier of E1:] = {} by A1, MCART_1:31; then A4: the Comp of E1 = {} .= the Comp of E2 by A3 ; A5: [: the carrier of E2, the carrier of E2:] = {} by A2, ZFMISC_1:90; [: the carrier of E1, the carrier of E1:] = {} by A1, ZFMISC_1:90; then the Arrows of E1 = {} .= the Arrows of E2 by A5 ; hence E1 = E2 by A1, A2, A4; ::_thesis: verum end; definition func the_empty_category -> strict AltCatStr means :Def10: :: ALTCAT_2:def 10 the carrier of it is empty ; existence ex b1 being strict AltCatStr st the carrier of b1 is empty proof reconsider a = {} as set ; set m = the ManySortedSet of [:a,a:]; set c = the BinComp of the ManySortedSet of [:a,a:]; take AltCatStr(# a, the ManySortedSet of [:a,a:], the BinComp of the ManySortedSet of [:a,a:] #) ; ::_thesis: the carrier of AltCatStr(# a, the ManySortedSet of [:a,a:], the BinComp of the ManySortedSet of [:a,a:] #) is empty thus the carrier of AltCatStr(# a, the ManySortedSet of [:a,a:], the BinComp of the ManySortedSet of [:a,a:] #) is empty ; ::_thesis: verum end; uniqueness for b1, b2 being strict AltCatStr st the carrier of b1 is empty & the carrier of b2 is empty holds b1 = b2 by Lm1; end; :: deftheorem Def10 defines the_empty_category ALTCAT_2:def_10_:_ for b1 being strict AltCatStr holds ( b1 = the_empty_category iff the carrier of b1 is empty ); registration cluster the_empty_category -> empty strict ; coherence the_empty_category is empty by Def10; end; registration cluster empty strict for AltCatStr ; existence ex b1 being AltCatStr st ( b1 is empty & b1 is strict ) proof take the_empty_category ; ::_thesis: ( the_empty_category is empty & the_empty_category is strict ) thus ( the_empty_category is empty & the_empty_category is strict ) ; ::_thesis: verum end; end; theorem :: ALTCAT_2:19 for E being empty strict AltCatStr holds E = the_empty_category by Lm1; begin definition let C be AltCatStr ; mode SubCatStr of C -> AltCatStr means :Def11: :: ALTCAT_2:def 11 ( the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C ); existence ex b1 being AltCatStr st ( the carrier of b1 c= the carrier of C & the Arrows of b1 cc= the Arrows of C & the Comp of b1 cc= the Comp of C ) ; end; :: deftheorem Def11 defines SubCatStr ALTCAT_2:def_11_:_ for C, b2 being AltCatStr holds ( b2 is SubCatStr of C iff ( the carrier of b2 c= the carrier of C & the Arrows of b2 cc= the Arrows of C & the Comp of b2 cc= the Comp of C ) ); theorem Th20: :: ALTCAT_2:20 for C being AltCatStr holds C is SubCatStr of C proof let C be AltCatStr ; ::_thesis: C is SubCatStr of C thus the carrier of C c= the carrier of C ; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C ) thus ( the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C ) ; ::_thesis: verum end; theorem :: ALTCAT_2:21 for C1, C2, C3 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C3 holds C1 is SubCatStr of C3 proof let C1, C2, C3 be AltCatStr ; ::_thesis: ( C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3 ) assume ( the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the carrier of C3 & the Arrows of C2 cc= the Arrows of C3 & the Comp of C2 cc= the Comp of C3 ) ; :: according to ALTCAT_2:def_11 ::_thesis: C1 is SubCatStr of C3 hence ( the carrier of C1 c= the carrier of C3 & the Arrows of C1 cc= the Arrows of C3 & the Comp of C1 cc= the Comp of C3 ) by Th8, XBOOLE_1:1; :: according to ALTCAT_2:def_11 ::_thesis: verum end; theorem Th22: :: ALTCAT_2:22 for C1, C2 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C1 holds AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) proof let C1, C2 be AltCatStr ; ::_thesis: ( C1 is SubCatStr of C2 & C2 is SubCatStr of C1 implies AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) ) assume that A1: ( the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 ) and A2: the Comp of C1 cc= the Comp of C2 and A3: ( the carrier of C2 c= the carrier of C1 & the Arrows of C2 cc= the Arrows of C1 ) and A4: the Comp of C2 cc= the Comp of C1 ; :: according to ALTCAT_2:def_11 ::_thesis: AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) ( the carrier of C1 = the carrier of C2 & the Arrows of C1 = the Arrows of C2 ) by A1, A3, Th7, XBOOLE_0:def_10; hence AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) by A2, A4, Th7; ::_thesis: verum end; registration let C be AltCatStr ; cluster strict for SubCatStr of C; existence ex b1 being SubCatStr of C st b1 is strict proof set D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #); reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by Def11; take D ; ::_thesis: D is strict thus D is strict ; ::_thesis: verum end; end; definition let C be non empty AltCatStr ; let o be object of C; func ObCat o -> strict SubCatStr of C means :Def12: :: ALTCAT_2:def 12 ( the carrier of it = {o} & the Arrows of it = (o,o) :-> <^o,o^> & the Comp of it = [o,o,o] .--> ( the Comp of C . (o,o,o)) ); existence ex b1 being strict SubCatStr of C st ( the carrier of b1 = {o} & the Arrows of b1 = (o,o) :-> <^o,o^> & the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) proof set m = [o,o,o] .--> ( the Comp of C . (o,o,o)); dom ([o,o,o] .--> ( the Comp of C . (o,o,o))) = {[o,o,o]} by FUNCOP_1:13 .= [:{o},{o},{o}:] by MCART_1:35 ; then reconsider m = [o,o,o] .--> ( the Comp of C . (o,o,o)) as ManySortedSet of [:{o},{o},{o}:] by PARTFUN1:def_2, RELAT_1:def_18; set a = (o,o) :-> <^o,o^>; dom ((o,o) :-> <^o,o^>) = [:{o},{o}:] by FUNCT_2:def_1; then reconsider a = (o,o) :-> <^o,o^> as ManySortedSet of [:{o},{o}:] by PARTFUN1:def_2; A1: a . (o,o) = the Arrows of C . (o,o) by ALTCAT_1:10; m is ManySortedFunction of {|a,a|},{|a|} proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [:{o},{o},{o}:] or m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] ) A2: o in {o} by TARSKI:def_1; assume i in [:{o},{o},{o}:] ; ::_thesis: m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] then i in {[o,o,o]} by MCART_1:35; then A3: i = [o,o,o] by TARSKI:def_1; then A4: {|a|} . i = {|a|} . (o,o,o) by MULTOP_1:def_1 .= the Arrows of C . (o,o) by A1, A2, ALTCAT_1:def_3 ; {|a,a|} . i = {|a,a|} . (o,o,o) by A3, MULTOP_1:def_1 .= [:( the Arrows of C . (o,o)),( the Arrows of C . (o,o)):] by A1, A2, ALTCAT_1:def_4 ; hence m . i is Element of bool [:({|a,a|} . i),({|a|} . i):] by A3, A4, FUNCOP_1:72; ::_thesis: verum end; then reconsider m = m as BinComp of a ; set D = AltCatStr(# {o},a,m #); AltCatStr(# {o},a,m #) is SubCatStr of C proof thus the carrier of AltCatStr(# {o},a,m #) c= the carrier of C ; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of AltCatStr(# {o},a,m #) cc= the Arrows of C & the Comp of AltCatStr(# {o},a,m #) cc= the Comp of C ) thus the Arrows of AltCatStr(# {o},a,m #) cc= the Arrows of C ::_thesis: the Comp of AltCatStr(# {o},a,m #) cc= the Comp of C proof thus [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] c= [: the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] holds the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i let i be set ; ::_thesis: ( i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] implies the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i ) assume i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] ; ::_thesis: the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i then i in {[o,o]} by ZFMISC_1:29; then i = [o,o] by TARSKI:def_1; hence the Arrows of AltCatStr(# {o},a,m #) . i c= the Arrows of C . i by A1; ::_thesis: verum end; thus [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] c= [: the carrier of C, the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] holds the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i let i be set ; ::_thesis: ( i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] implies the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i ) assume i in [: the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #), the carrier of AltCatStr(# {o},a,m #):] ; ::_thesis: the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i then i in {[o,o,o]} by MCART_1:35; then A5: i = [o,o,o] by TARSKI:def_1; then the Comp of AltCatStr(# {o},a,m #) . i = the Comp of C . (o,o,o) by FUNCOP_1:72 .= the Comp of C . i by A5, MULTOP_1:def_1 ; hence the Comp of AltCatStr(# {o},a,m #) . i c= the Comp of C . i ; ::_thesis: verum end; then reconsider D = AltCatStr(# {o},a,m #) as strict SubCatStr of C ; take D ; ::_thesis: ( the carrier of D = {o} & the Arrows of D = (o,o) :-> <^o,o^> & the Comp of D = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) thus ( the carrier of D = {o} & the Arrows of D = (o,o) :-> <^o,o^> & the Comp of D = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict SubCatStr of C st the carrier of b1 = {o} & the Arrows of b1 = (o,o) :-> <^o,o^> & the Comp of b1 = [o,o,o] .--> ( the Comp of C . (o,o,o)) & the carrier of b2 = {o} & the Arrows of b2 = (o,o) :-> <^o,o^> & the Comp of b2 = [o,o,o] .--> ( the Comp of C . (o,o,o)) holds b1 = b2 ; end; :: deftheorem Def12 defines ObCat ALTCAT_2:def_12_:_ for C being non empty AltCatStr for o being object of C for b3 being strict SubCatStr of C holds ( b3 = ObCat o iff ( the carrier of b3 = {o} & the Arrows of b3 = (o,o) :-> <^o,o^> & the Comp of b3 = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) ); theorem Th23: :: ALTCAT_2:23 for C being non empty AltCatStr for o being object of C for o9 being object of (ObCat o) holds o9 = o proof let C be non empty AltCatStr ; ::_thesis: for o being object of C for o9 being object of (ObCat o) holds o9 = o let o be object of C; ::_thesis: for o9 being object of (ObCat o) holds o9 = o let o9 be object of (ObCat o); ::_thesis: o9 = o the carrier of (ObCat o) = {o} by Def12; hence o9 = o by TARSKI:def_1; ::_thesis: verum end; registration let C be non empty AltCatStr ; let o be object of C; cluster ObCat o -> non empty transitive strict ; coherence ( ObCat o is transitive & not ObCat o is empty ) proof thus ObCat o is transitive ::_thesis: not ObCat o is empty proof let o1, o2, o3 be object of (ObCat o); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) assume that <^o1,o2^> <> {} and A1: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {} o1 = o by Th23; hence not <^o1,o3^> = {} by A1, Th23; ::_thesis: verum end; the carrier of (ObCat o) = {o} by Def12; hence not the carrier of (ObCat o) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; registration let C be non empty AltCatStr ; cluster non empty transitive strict for SubCatStr of C; existence ex b1 being SubCatStr of C st ( b1 is transitive & not b1 is empty & b1 is strict ) proof set o = the object of C; take ObCat the object of C ; ::_thesis: ( ObCat the object of C is transitive & not ObCat the object of C is empty & ObCat the object of C is strict ) thus ( ObCat the object of C is transitive & not ObCat the object of C is empty & ObCat the object of C is strict ) ; ::_thesis: verum end; end; theorem Th24: :: ALTCAT_2:24 for C being non empty transitive AltCatStr for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds D1 is SubCatStr of D2 proof let C be non empty transitive AltCatStr ; ::_thesis: for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds D1 is SubCatStr of D2 let D1, D2 be non empty transitive SubCatStr of C; ::_thesis: ( the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 implies D1 is SubCatStr of D2 ) assume that A1: the carrier of D1 c= the carrier of D2 and A2: the Arrows of D1 cc= the Arrows of D2 ; ::_thesis: D1 is SubCatStr of D2 thus the carrier of D1 c= the carrier of D2 by A1; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of D1 cc= the Arrows of D2 & the Comp of D1 cc= the Comp of D2 ) thus the Arrows of D1 cc= the Arrows of D2 by A2; ::_thesis: the Comp of D1 cc= the Comp of D2 thus [: the carrier of D1, the carrier of D1, the carrier of D1:] c= [: the carrier of D2, the carrier of D2, the carrier of D2:] by A1, MCART_1:73; :: according to ALTCAT_2:def_2 ::_thesis: for i being set st i in [: the carrier of D1, the carrier of D1, the carrier of D1:] holds the Comp of D1 . i c= the Comp of D2 . i let x be set ; ::_thesis: ( x in [: the carrier of D1, the carrier of D1, the carrier of D1:] implies the Comp of D1 . x c= the Comp of D2 . x ) assume A3: x in [: the carrier of D1, the carrier of D1, the carrier of D1:] ; ::_thesis: the Comp of D1 . x c= the Comp of D2 . x then consider i1, i2, i3 being set such that A4: ( i1 in the carrier of D1 & i2 in the carrier of D1 & i3 in the carrier of D1 ) and A5: x = [i1,i2,i3] by MCART_1:68; reconsider i1 = i1, i2 = i2, i3 = i3 as object of D1 by A4; reconsider j1 = i1, j2 = i2, j3 = i3 as object of D2 by A1, A4; [i2,i3] in [: the carrier of D1, the carrier of D1:] ; then A6: <^i2,i3^> c= <^j2,j3^> by A2, Def2; reconsider c2 = the Comp of D2 . (j1,j2,j3) as Function of [:<^j2,j3^>,<^j1,j2^>:],<^j1,j3^> ; reconsider c1 = the Comp of D1 . (i1,i2,i3) as Function of [:<^i2,i3^>,<^i1,i2^>:],<^i1,i3^> ; ( not <^i1,i3^> = {} or <^i2,i3^> = {} or <^i1,i2^> = {} ) by ALTCAT_1:def_2; then ( <^i1,i3^> = {} implies [:<^i2,i3^>,<^i1,i2^>:] = {} ) by ZFMISC_1:90; then A7: dom c1 = [:<^i2,i3^>,<^i1,i2^>:] by FUNCT_2:def_1; ( not <^j1,j3^> = {} or <^j2,j3^> = {} or <^j1,j2^> = {} ) by ALTCAT_1:def_2; then ( <^j1,j3^> = {} implies [:<^j2,j3^>,<^j1,j2^>:] = {} ) by ZFMISC_1:90; then A8: dom c2 = [:<^j2,j3^>,<^j1,j2^>:] by FUNCT_2:def_1; [i1,i2] in [: the carrier of D1, the carrier of D1:] ; then <^i1,i2^> c= <^j1,j2^> by A2, Def2; then A9: dom c1 c= dom c2 by A7, A6, A8, ZFMISC_1:96; A10: now__::_thesis:_for_y_being_set_st_y_in_dom_c1_holds_ c1_._y_=_c2_._y the carrier of D1 c= the carrier of C by Def11; then reconsider o1 = i1, o2 = i2, o3 = i3 as object of C by A4; reconsider c = the Comp of C . (o1,o2,o3) as Function of [:<^o2,o3^>,<^o1,o2^>:],<^o1,o3^> ; let y be set ; ::_thesis: ( y in dom c1 implies c1 . y = c2 . y ) A11: c = the Comp of C . [o1,o2,o3] by MULTOP_1:def_1; A12: c2 = the Comp of D2 . [o1,o2,o3] by MULTOP_1:def_1; ( [o1,o2,o3] in [: the carrier of D2, the carrier of D2, the carrier of D2:] & the Comp of D2 cc= the Comp of C ) by A1, A4, Def11, MCART_1:69; then A13: c2 c= c by A11, A12, Def2; assume A14: y in dom c1 ; ::_thesis: c1 . y = c2 . y ( the Comp of D1 cc= the Comp of C & c1 = the Comp of D1 . [o1,o2,o3] ) by Def11, MULTOP_1:def_1; then c1 c= c by A3, A5, A11, Def2; hence c1 . y = c . y by A14, GRFUNC_1:2 .= c2 . y by A9, A14, A13, GRFUNC_1:2 ; ::_thesis: verum end; ( c1 = the Comp of D1 . x & c2 = the Comp of D2 . x ) by A5, MULTOP_1:def_1; hence the Comp of D1 . x c= the Comp of D2 . x by A9, A10, GRFUNC_1:2; ::_thesis: verum end; definition let C be AltCatStr ; let D be SubCatStr of C; attrD is full means :Def13: :: ALTCAT_2:def 13 the Arrows of D = the Arrows of C || the carrier of D; end; :: deftheorem Def13 defines full ALTCAT_2:def_13_:_ for C being AltCatStr for D being SubCatStr of C holds ( D is full iff the Arrows of D = the Arrows of C || the carrier of D ); definition let C be non empty with_units AltCatStr ; let D be SubCatStr of C; attrD is id-inheriting means :Def14: :: ALTCAT_2:def 14 for o being object of D for o9 being object of C st o = o9 holds idm o9 in <^o,o^> if not D is empty otherwise verum; consistency verum ; end; :: deftheorem Def14 defines id-inheriting ALTCAT_2:def_14_:_ for C being non empty with_units AltCatStr for D being SubCatStr of C holds ( ( not D is empty implies ( D is id-inheriting iff for o being object of D for o9 being object of C st o = o9 holds idm o9 in <^o,o^> ) ) & ( D is empty implies ( D is id-inheriting iff verum ) ) ); registration let C be AltCatStr ; cluster strict full for SubCatStr of C; existence ex b1 being SubCatStr of C st ( b1 is full & b1 is strict ) proof set D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #); reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by Def11; take D ; ::_thesis: ( D is full & D is strict ) dom the Arrows of C = [: the carrier of D, the carrier of D:] by PARTFUN1:def_2; hence the Arrows of D = the Arrows of C || the carrier of D by RELAT_1:69; :: according to ALTCAT_2:def_13 ::_thesis: D is strict thus D is strict ; ::_thesis: verum end; end; registration let C be non empty AltCatStr ; cluster non empty strict full for SubCatStr of C; existence ex b1 being SubCatStr of C st ( b1 is full & not b1 is empty & b1 is strict ) proof set D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #); reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by Def11; take D ; ::_thesis: ( D is full & not D is empty & D is strict ) dom the Arrows of C = [: the carrier of D, the carrier of D:] by PARTFUN1:def_2; hence the Arrows of D = the Arrows of C || the carrier of D by RELAT_1:69; :: according to ALTCAT_2:def_13 ::_thesis: ( not D is empty & D is strict ) thus not the carrier of D is empty ; :: according to STRUCT_0:def_1 ::_thesis: D is strict thus D is strict ; ::_thesis: verum end; end; registration let C be category; let o be object of C; cluster ObCat o -> strict full id-inheriting ; coherence ( ObCat o is full & ObCat o is id-inheriting ) proof A1: the carrier of (ObCat o) = {o} by Def12; the Arrows of (ObCat o) = (o,o) :-> <^o,o^> by Def12 .= the Arrows of C || the carrier of (ObCat o) by A1, FUNCT_7:8 ; hence ObCat o is full by Def13; ::_thesis: ObCat o is id-inheriting now__::_thesis:_for_o1_being_object_of_(ObCat_o) for_o2_being_object_of_C_st_o1_=_o2_holds_ idm_o2_in_<^o1,o1^> let o1 be object of (ObCat o); ::_thesis: for o2 being object of C st o1 = o2 holds idm o2 in <^o1,o1^> let o2 be object of C; ::_thesis: ( o1 = o2 implies idm o2 in <^o1,o1^> ) assume A2: o1 = o2 ; ::_thesis: idm o2 in <^o1,o1^> A3: o1 = o by Th23; then <^o1,o1^> = ((o,o) :-> <^o,o^>) . (o,o) by Def12 .= <^o2,o2^> by A3, A2, ALTCAT_1:10 ; hence idm o2 in <^o1,o1^> by ALTCAT_1:19; ::_thesis: verum end; hence ObCat o is id-inheriting by Def14; ::_thesis: verum end; end; registration let C be category; cluster non empty strict full id-inheriting for SubCatStr of C; existence ex b1 being SubCatStr of C st ( b1 is full & b1 is id-inheriting & not b1 is empty & b1 is strict ) proof set o = the object of C; take ObCat the object of C ; ::_thesis: ( ObCat the object of C is full & ObCat the object of C is id-inheriting & not ObCat the object of C is empty & ObCat the object of C is strict ) thus ( ObCat the object of C is full & ObCat the object of C is id-inheriting & not ObCat the object of C is empty & ObCat the object of C is strict ) ; ::_thesis: verum end; end; theorem Th25: :: ALTCAT_2:25 for C being non empty transitive AltCatStr for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) proof let C be non empty transitive AltCatStr ; ::_thesis: for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) let D be SubCatStr of C; ::_thesis: ( the carrier of D = the carrier of C & the Arrows of D = the Arrows of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) ) assume that A1: the carrier of D = the carrier of C and A2: the Arrows of D = the Arrows of C ; ::_thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) A3: D is transitive proof let o1, o2, o3 be object of D; :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) reconsider p1 = o1, p2 = o2, p3 = o3 as object of C by A1; assume A4: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: not <^o1,o3^> = {} A5: <^o1,o3^> = <^p1,p3^> by A2; ( <^o1,o2^> = <^p1,p2^> & <^o2,o3^> = <^p2,p3^> ) by A2; hence not <^o1,o3^> = {} by A5, A4, ALTCAT_1:def_2; ::_thesis: verum end; A6: C is SubCatStr of C by Th20; not D is empty by A1; then C is SubCatStr of D by A1, A2, A3, A6, Th24; hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Th22; ::_thesis: verum end; theorem Th26: :: ALTCAT_2:26 for C being non empty transitive AltCatStr for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) proof let C be non empty transitive AltCatStr ; ::_thesis: for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) let D1, D2 be non empty transitive SubCatStr of C; ::_thesis: ( the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 implies AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) ) assume ( the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 ) ; ::_thesis: AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) then ( D1 is SubCatStr of D2 & D2 is SubCatStr of D1 ) by Th24; hence AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) by Th22; ::_thesis: verum end; theorem :: ALTCAT_2:27 for C being non empty transitive AltCatStr for D being full SubCatStr of C st the carrier of D = the carrier of C holds AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) proof let C be non empty transitive AltCatStr ; ::_thesis: for D being full SubCatStr of C st the carrier of D = the carrier of C holds AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) let D be full SubCatStr of C; ::_thesis: ( the carrier of D = the carrier of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) ) assume A1: the carrier of D = the carrier of C ; ::_thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) A2: dom the Arrows of C = [: the carrier of C, the carrier of C:] by PARTFUN1:def_2; the Arrows of D = the Arrows of C || the carrier of D by Def13 .= the Arrows of C by A1, A2, RELAT_1:69 ; hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by A1, Th25; ::_thesis: verum end; theorem Th28: :: ALTCAT_2:28 for C being non empty AltCatStr for D being non empty full SubCatStr of C for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^o1,o2^> = <^p1,p2^> proof let C be non empty AltCatStr ; ::_thesis: for D being non empty full SubCatStr of C for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^o1,o2^> = <^p1,p2^> let D be non empty full SubCatStr of C; ::_thesis: for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^o1,o2^> = <^p1,p2^> let o1, o2 be object of C; ::_thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^o1,o2^> = <^p1,p2^> let p1, p2 be object of D; ::_thesis: ( o1 = p1 & o2 = p2 implies <^o1,o2^> = <^p1,p2^> ) assume A1: ( o1 = p1 & o2 = p2 ) ; ::_thesis: <^o1,o2^> = <^p1,p2^> [p1,p2] in [: the carrier of D, the carrier of D:] ; hence <^o1,o2^> = ( the Arrows of C || the carrier of D) . (p1,p2) by A1, FUNCT_1:49 .= <^p1,p2^> by Def13 ; ::_thesis: verum end; theorem Th29: :: ALTCAT_2:29 for C being non empty AltCatStr for D being non empty SubCatStr of C for o being object of D holds o is object of C proof let C be non empty AltCatStr ; ::_thesis: for D being non empty SubCatStr of C for o being object of D holds o is object of C let D be non empty SubCatStr of C; ::_thesis: for o being object of D holds o is object of C let o be object of D; ::_thesis: o is object of C ( o in the carrier of D & the carrier of D c= the carrier of C ) by Def11; hence o is object of C ; ::_thesis: verum end; registration let C be non empty transitive AltCatStr ; cluster non empty full -> transitive for SubCatStr of C; coherence for b1 being SubCatStr of C st b1 is full & not b1 is empty holds b1 is transitive proof let D be SubCatStr of C; ::_thesis: ( D is full & not D is empty implies D is transitive ) assume A1: ( D is full & not D is empty ) ; ::_thesis: D is transitive let o1, o2, o3 be object of D; :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: not <^o1,o3^> = {} reconsider p1 = o1, p2 = o2, p3 = o3 as object of C by A1, Th29; ( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) by A1, A2, Th28; then <^p1,p3^> <> {} by ALTCAT_1:def_2; hence not <^o1,o3^> = {} by A1, Th28; ::_thesis: verum end; end; theorem :: ALTCAT_2:30 for C being non empty transitive AltCatStr for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) proof let C be non empty transitive AltCatStr ; ::_thesis: for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) let D1, D2 be non empty full SubCatStr of C; ::_thesis: ( the carrier of D1 = the carrier of D2 implies AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) ) assume A1: the carrier of D1 = the carrier of D2 ; ::_thesis: AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) then the Arrows of D1 = the Arrows of C || the carrier of D2 by Def13 .= the Arrows of D2 by Def13 ; hence AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) by A1, Th26; ::_thesis: verum end; theorem Th31: :: ALTCAT_2:31 for C being non empty AltCatStr for D being non empty SubCatStr of C for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^p1,p2^> c= <^o1,o2^> proof let C be non empty AltCatStr ; ::_thesis: for D being non empty SubCatStr of C for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^p1,p2^> c= <^o1,o2^> let D be non empty SubCatStr of C; ::_thesis: for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^p1,p2^> c= <^o1,o2^> let o1, o2 be object of C; ::_thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 holds <^p1,p2^> c= <^o1,o2^> let p1, p2 be object of D; ::_thesis: ( o1 = p1 & o2 = p2 implies <^p1,p2^> c= <^o1,o2^> ) assume A1: ( o1 = p1 & o2 = p2 ) ; ::_thesis: <^p1,p2^> c= <^o1,o2^> ( [p1,p2] in [: the carrier of D, the carrier of D:] & the Arrows of D cc= the Arrows of C ) by Def11; hence <^p1,p2^> c= <^o1,o2^> by A1, Def2; ::_thesis: verum end; theorem Th32: :: ALTCAT_2:32 for C being non empty transitive AltCatStr for D being non empty transitive SubCatStr of C for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff proof let C be non empty transitive AltCatStr ; ::_thesis: for D being non empty transitive SubCatStr of C for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let D be non empty transitive SubCatStr of C; ::_thesis: for p1, p2, p3 being object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let p1, p2, p3 be object of D; ::_thesis: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} implies for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff ) assume A1: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) ; ::_thesis: for o1, o2, o3 being object of C st o1 = p1 & o2 = p2 & o3 = p3 holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let o1, o2, o3 be object of C; ::_thesis: ( o1 = p1 & o2 = p2 & o3 = p3 implies for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff ) assume A2: ( o1 = p1 & o2 = p2 & o3 = p3 ) ; ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let g be Morphism of o2,o3; ::_thesis: for ff being Morphism of p1,p2 for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let ff be Morphism of p1,p2; ::_thesis: for gg being Morphism of p2,p3 st f = ff & g = gg holds g * f = gg * ff let gg be Morphism of p2,p3; ::_thesis: ( f = ff & g = gg implies g * f = gg * ff ) assume A3: ( f = ff & g = gg ) ; ::_thesis: g * f = gg * ff <^p1,p3^> <> {} by A1, ALTCAT_1:def_2; then dom ( the Comp of D . (p1,p2,p3)) = [:<^p2,p3^>,<^p1,p2^>:] by FUNCT_2:def_1; then A4: [gg,ff] in dom ( the Comp of D . (p1,p2,p3)) by A1, ZFMISC_1:87; A5: the Comp of D cc= the Comp of C by Def11; ( the Comp of D . (p1,p2,p3) = the Comp of D . [p1,p2,p3] & the Comp of C . (o1,o2,o3) = the Comp of C . [o1,o2,o3] ) by MULTOP_1:def_1; then A6: the Comp of D . (p1,p2,p3) c= the Comp of C . (o1,o2,o3) by A2, A5, Def2; ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) by A1, A2, Th31, XBOOLE_1:3; hence g * f = ( the Comp of C . (o1,o2,o3)) . (g,f) by ALTCAT_1:def_8 .= ( the Comp of D . (p1,p2,p3)) . (gg,ff) by A3, A4, A6, GRFUNC_1:2 .= gg * ff by A1, ALTCAT_1:def_8 ; ::_thesis: verum end; registration let C be non empty transitive associative AltCatStr ; cluster non empty transitive -> non empty associative for SubCatStr of C; coherence for b1 being non empty SubCatStr of C st b1 is transitive holds b1 is associative proof let D be non empty SubCatStr of C; ::_thesis: ( D is transitive implies D is associative ) assume D is transitive ; ::_thesis: D is associative then reconsider D = D as non empty transitive SubCatStr of C ; D is associative proof let o1, o2, o3, o4 be object of D; :: according to ALTCAT_2:def_8 ::_thesis: for f being Morphism of o1,o2 for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) A1: ( o1 in the carrier of D & o2 in the carrier of D ) ; A2: ( o3 in the carrier of D & o4 in the carrier of D ) ; the carrier of D c= the carrier of C by Def11; then reconsider p1 = o1, p2 = o2, p3 = o3, p4 = o4 as object of C by A1, A2; let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) let g be Morphism of o2,o3; ::_thesis: for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds (h * g) * f = h * (g * f) let h be Morphism of o3,o4; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies (h * g) * f = h * (g * f) ) assume that A3: <^o1,o2^> <> {} and A4: <^o2,o3^> <> {} and A5: <^o3,o4^> <> {} ; ::_thesis: (h * g) * f = h * (g * f) A6: <^o2,o3^> c= <^p2,p3^> by Th31; g in <^o2,o3^> by A4; then reconsider gg = g as Morphism of p2,p3 by A6; A7: <^o1,o2^> c= <^p1,p2^> by Th31; f in <^o1,o2^> by A3; then reconsider ff = f as Morphism of p1,p2 by A7; A8: ( <^o1,o3^> <> {} & g * f = gg * ff ) by A3, A4, Th32, ALTCAT_1:def_2; A9: <^o3,o4^> c= <^p3,p4^> by Th31; h in <^o3,o4^> by A5; then reconsider hh = h as Morphism of p3,p4 by A9; A10: <^p3,p4^> <> {} by A5, Th31, XBOOLE_1:3; A11: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) by A3, A4, Th31, XBOOLE_1:3; ( <^o2,o4^> <> {} & h * g = hh * gg ) by A4, A5, Th32, ALTCAT_1:def_2; hence (h * g) * f = (hh * gg) * ff by A3, Th32 .= hh * (gg * ff) by A11, A10, Def8 .= h * (g * f) by A5, A8, Th32 ; ::_thesis: verum end; hence D is associative ; ::_thesis: verum end; end; theorem Th33: :: ALTCAT_2:33 for C being non empty AltCatStr for D being non empty SubCatStr of C for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds for n being Morphism of p1,p2 holds n is Morphism of o1,o2 proof let C be non empty AltCatStr ; ::_thesis: for D being non empty SubCatStr of C for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds for n being Morphism of p1,p2 holds n is Morphism of o1,o2 let D be non empty SubCatStr of C; ::_thesis: for o1, o2 being object of C for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds for n being Morphism of p1,p2 holds n is Morphism of o1,o2 let o1, o2 be object of C; ::_thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds for n being Morphism of p1,p2 holds n is Morphism of o1,o2 let p1, p2 be object of D; ::_thesis: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} implies for n being Morphism of p1,p2 holds n is Morphism of o1,o2 ) assume A1: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} ) ; ::_thesis: for n being Morphism of p1,p2 holds n is Morphism of o1,o2 let n be Morphism of p1,p2; ::_thesis: n is Morphism of o1,o2 ( n in <^p1,p2^> & <^p1,p2^> c= <^o1,o2^> ) by A1, Th31; hence n is Morphism of o1,o2 ; ::_thesis: verum end; registration let C be non empty transitive with_units AltCatStr ; cluster non empty transitive id-inheriting -> non empty with_units for SubCatStr of C; coherence for b1 being non empty SubCatStr of C st b1 is id-inheriting & b1 is transitive holds b1 is with_units proof let D be non empty SubCatStr of C; ::_thesis: ( D is id-inheriting & D is transitive implies D is with_units ) assume that A1: D is id-inheriting and A2: D is transitive ; ::_thesis: D is with_units let o be object of D; :: according to ALTCAT_2:def_9 ::_thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being object of D for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) reconsider p = o as object of C by Th29; reconsider i = idm p as Morphism of o,o by A1, Def14; A3: idm p in <^o,o^> by A1, Def14; hence <^o,o^> <> {} ; ::_thesis: ex i being Morphism of o,o st for o9 being object of D for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) take i ; ::_thesis: for o9 being object of D for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) let o9 be object of D; ::_thesis: for m9 being Morphism of o9,o for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) let m9 be Morphism of o9,o; ::_thesis: for m99 being Morphism of o,o9 holds ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) let m99 be Morphism of o,o9; ::_thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) hereby ::_thesis: ( <^o,o9^> <> {} implies m99 * i = m99 ) reconsider p9 = o9 as object of C by Th29; assume A4: <^o9,o^> <> {} ; ::_thesis: i * m9 = m9 then A5: <^p9,p^> <> {} by Th31, XBOOLE_1:3; reconsider n9 = m9 as Morphism of p9,p by A4, Th33; thus i * m9 = (idm p) * n9 by A2, A3, A4, Th32 .= m9 by A5, ALTCAT_1:20 ; ::_thesis: verum end; reconsider p9 = o9 as object of C by Th29; assume A6: <^o,o9^> <> {} ; ::_thesis: m99 * i = m99 then A7: <^p,p9^> <> {} by Th31, XBOOLE_1:3; reconsider n99 = m99 as Morphism of p,p9 by A6, Th33; thus m99 * i = n99 * (idm p) by A2, A3, A6, Th32 .= m99 by A7, ALTCAT_1:def_17 ; ::_thesis: verum end; end; registration let C be category; cluster non empty transitive id-inheriting for SubCatStr of C; existence ex b1 being non empty SubCatStr of C st ( b1 is id-inheriting & b1 is transitive ) proof set o = the object of C; take ObCat the object of C ; ::_thesis: ( ObCat the object of C is id-inheriting & ObCat the object of C is transitive ) thus ( ObCat the object of C is id-inheriting & ObCat the object of C is transitive ) ; ::_thesis: verum end; end; definition let C be category; mode subcategory of C is transitive id-inheriting SubCatStr of C; end; theorem :: ALTCAT_2:34 for C being category for D being non empty subcategory of C for o being object of D for o9 being object of C st o = o9 holds idm o = idm o9 proof let C be category; ::_thesis: for D being non empty subcategory of C for o being object of D for o9 being object of C st o = o9 holds idm o = idm o9 let D be non empty subcategory of C; ::_thesis: for o being object of D for o9 being object of C st o = o9 holds idm o = idm o9 let o be object of D; ::_thesis: for o9 being object of C st o = o9 holds idm o = idm o9 let o9 be object of C; ::_thesis: ( o = o9 implies idm o = idm o9 ) assume A1: o = o9 ; ::_thesis: idm o = idm o9 then reconsider m = idm o9 as Morphism of o,o by Def14; A2: idm o9 in <^o,o^> by A1, Def14; now__::_thesis:_for_p_being_object_of_D_st_<^o,p^>_<>_{}_holds_ for_a_being_Morphism_of_o,p_holds_a_*_m_=_a let p be object of D; ::_thesis: ( <^o,p^> <> {} implies for a being Morphism of o,p holds a * m = a ) assume A3: <^o,p^> <> {} ; ::_thesis: for a being Morphism of o,p holds a * m = a reconsider p9 = p as object of C by Th29; A4: <^o9,p9^> <> {} by A1, A3, Th31, XBOOLE_1:3; let a be Morphism of o,p; ::_thesis: a * m = a reconsider n = a as Morphism of o9,p9 by A1, A3, Th33; thus a * m = n * (idm o9) by A1, A2, A3, Th32 .= a by A4, ALTCAT_1:def_17 ; ::_thesis: verum end; hence idm o = idm o9 by ALTCAT_1:def_17; ::_thesis: verum end;