:: CATALG_1 semantic presentation begin definition let I be set ; let A, f be Function; funcf -MSF (I,A) -> ManySortedFunction of I means :Def1: :: CATALG_1:def 1 for i being set st i in I holds it . i = f | (A . i); existence ex b1 being ManySortedFunction of I st for i being set st i in I holds b1 . i = f | (A . i) proof deffunc H1( set ) -> set = f | (A . \$1); consider F being ManySortedSet of I such that A1: for i being set st i in I holds F . i = H1(i) from PBOOLE:sch_4(); F is Function-yielding proof let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 F or F . x is set ) assume x in dom F ; ::_thesis: F . x is set then x in I ; then F . x = f | (A . x) by A1; hence F . x is set ; ::_thesis: verum end; hence ex b1 being ManySortedFunction of I st for i being set st i in I holds b1 . i = f | (A . i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of I st ( for i being set st i in I holds b1 . i = f | (A . i) ) & ( for i being set st i in I holds b2 . i = f | (A . i) ) holds b1 = b2 proof let g1, g2 be ManySortedFunction of I; ::_thesis: ( ( for i being set st i in I holds g1 . i = f | (A . i) ) & ( for i being set st i in I holds g2 . i = f | (A . i) ) implies g1 = g2 ) assume that A2: for i being set st i in I holds g1 . i = f | (A . i) and A3: for i being set st i in I holds g2 . i = f | (A . i) ; ::_thesis: g1 = g2 now__::_thesis:_for_i_being_set_st_i_in_I_holds_ g1_._i_=_g2_._i let i be set ; ::_thesis: ( i in I implies g1 . i = g2 . i ) assume A4: i in I ; ::_thesis: g1 . i = g2 . i then g1 . i = f | (A . i) by A2; hence g1 . i = g2 . i by A3, A4; ::_thesis: verum end; hence g1 = g2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def1 defines -MSF CATALG_1:def_1_:_ for I being set for A, f being Function for b4 being ManySortedFunction of I holds ( b4 = f -MSF (I,A) iff for i being set st i in I holds b4 . i = f | (A . i) ); theorem :: CATALG_1:1 for I being set for A being ManySortedSet of I holds (id (Union A)) -MSF (I,A) = id A proof let I be set ; ::_thesis: for A being ManySortedSet of I holds (id (Union A)) -MSF (I,A) = id A let A be ManySortedSet of I; ::_thesis: (id (Union A)) -MSF (I,A) = id A set f = id (Union A); set F = (id (Union A)) -MSF (I,A); now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((id_(Union_A))_-MSF_(I,A))_._i_=_(id_A)_._i let i be set ; ::_thesis: ( i in I implies ((id (Union A)) -MSF (I,A)) . i = (id A) . i ) A1: Union A = union (rng A) by CARD_3:def_4; assume A2: i in I ; ::_thesis: ((id (Union A)) -MSF (I,A)) . i = (id A) . i then i in dom A by PARTFUN1:def_2; then A3: A . i in rng A by FUNCT_1:def_3; ( ((id (Union A)) -MSF (I,A)) . i = (id (Union A)) | (A . i) & (id A) . i = id (A . i) ) by A2, Def1, MSUALG_3:def_1; hence ((id (Union A)) -MSF (I,A)) . i = (id A) . i by A3, A1, FUNCT_3:1, ZFMISC_1:74; ::_thesis: verum end; hence (id (Union A)) -MSF (I,A) = id A by PBOOLE:3; ::_thesis: verum end; theorem :: CATALG_1:2 for I being set for A, B being ManySortedSet of I for f, g being Function st rngs (f -MSF (I,A)) c= B holds (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for f, g being Function st rngs (f -MSF (I,A)) c= B holds (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) let A, B be ManySortedSet of I; ::_thesis: for f, g being Function st rngs (f -MSF (I,A)) c= B holds (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) let f, g be Function; ::_thesis: ( rngs (f -MSF (I,A)) c= B implies (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) ) assume A1: rngs (f -MSF (I,A)) c= B ; ::_thesis: (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) A2: I /\ I = I ; ( dom (g -MSF (I,B)) = I & dom (f -MSF (I,A)) = I ) by PARTFUN1:def_2; then A3: dom ((g -MSF (I,B)) ** (f -MSF (I,A))) = I by A2, PBOOLE:def_19; A4: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((g_*_f)_-MSF_(I,A))_._i_=_((g_-MSF_(I,B))_**_(f_-MSF_(I,A)))_._i let i be set ; ::_thesis: ( i in I implies ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i ) assume A5: i in I ; ::_thesis: ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i then A6: (f -MSF (I,A)) . i = f | (A . i) by Def1; dom (f -MSF (I,A)) = I by PARTFUN1:def_2; then (rngs (f -MSF (I,A))) . i = rng (f | (A . i)) by A5, A6, FUNCT_6:22; then rng (f | (A . i)) c= B . i by A1, A5, PBOOLE:def_2; then ( (g * f) | (A . i) = g * (f | (A . i)) & (B . i) |` (f | (A . i)) = f | (A . i) ) by RELAT_1:83, RELAT_1:94; then A7: (g * f) | (A . i) = (g | (B . i)) * (f | (A . i)) by MONOID_1:1; ( ((g * f) -MSF (I,A)) . i = (g * f) | (A . i) & (g -MSF (I,B)) . i = g | (B . i) ) by A5, Def1; hence ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i by A3, A5, A6, A7, PBOOLE:def_19; ::_thesis: verum end; dom ((g * f) -MSF (I,A)) = I by PARTFUN1:def_2; hence (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) by A3, A4, FUNCT_1:2; ::_thesis: verum end; theorem :: CATALG_1:3 for f being Function for I being set for A, B being ManySortedSet of I st ( for i being set st i in I holds ( A . i c= dom f & f .: (A . i) c= B . i ) ) holds f -MSF (I,A) is ManySortedFunction of A,B proof let f be Function; ::_thesis: for I being set for A, B being ManySortedSet of I st ( for i being set st i in I holds ( A . i c= dom f & f .: (A . i) c= B . i ) ) holds f -MSF (I,A) is ManySortedFunction of A,B let I be set ; ::_thesis: for A, B being ManySortedSet of I st ( for i being set st i in I holds ( A . i c= dom f & f .: (A . i) c= B . i ) ) holds f -MSF (I,A) is ManySortedFunction of A,B let A, B be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds ( A . i c= dom f & f .: (A . i) c= B . i ) ) implies f -MSF (I,A) is ManySortedFunction of A,B ) assume A1: for i being set st i in I holds ( A . i c= dom f & f .: (A . i) c= B . i ) ; ::_thesis: f -MSF (I,A) is ManySortedFunction of A,B let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] ) assume A2: i in I ; ::_thesis: (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] then A3: (f -MSF (I,A)) . i = f | (A . i) by Def1; f .: (A . i) c= B . i by A1, A2; then A4: rng ((f -MSF (I,A)) . i) c= B . i by A3, RELAT_1:115; dom ((f -MSF (I,A)) . i) = A . i by A1, A2, A3, RELAT_1:62; hence (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; ::_thesis: verum end; Lm1: now__::_thesis:_for_x,_y_being_set_st_<*x*>_=_<*y*>_holds_ x_=_y let x, y be set ; ::_thesis: ( <*x*> = <*y*> implies x = y ) assume <*x*> = <*y*> ; ::_thesis: x = y then <*x*> . 1 = y by FINSEQ_1:40; hence x = y by FINSEQ_1:40; ::_thesis: verum end; definition let S be non empty ManySortedSign ; let A be MSAlgebra over S; attrA is empty means :Def2: :: CATALG_1:def 2 the Sorts of A is V3(); end; :: deftheorem Def2 defines empty CATALG_1:def_2_:_ for S being non empty ManySortedSign for A being MSAlgebra over S holds ( A is empty iff the Sorts of A is V3() ); registration let S be non empty ManySortedSign ; cluster non-empty -> non empty for MSAlgebra over S; coherence for b1 being MSAlgebra over S st b1 is non-empty holds not b1 is empty proof let A be MSAlgebra over S; ::_thesis: ( A is non-empty implies not A is empty ) assume the Sorts of A is V2() ; :: according to MSUALG_1:def_3 ::_thesis: not A is empty hence the Sorts of A is V3() ; :: according to CATALG_1:def_2 ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; cluster strict non-empty disjoint_valued for MSAlgebra over S; existence ex b1 being MSAlgebra over S st ( b1 is strict & b1 is non-empty & b1 is disjoint_valued ) proof set X = the V2() ManySortedSet of the carrier of S; take FreeMSA the V2() ManySortedSet of the carrier of S ; ::_thesis: ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is disjoint_valued ) thus ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is disjoint_valued ) ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let A be non empty MSAlgebra over S; cluster the Sorts of A -> V3() ; coherence not the Sorts of A is empty-yielding by Def2; end; registration cluster Relation-like non empty-yielding Function-like for set ; existence not for b1 being Function holds b1 is empty-yielding proof set S = the non empty non void ManySortedSign ; set A = the non empty MSAlgebra over the non empty non void ManySortedSign ; take the Sorts of the non empty MSAlgebra over the non empty non void ManySortedSign ; ::_thesis: not the Sorts of the non empty MSAlgebra over the non empty non void ManySortedSign is empty-yielding thus not the Sorts of the non empty MSAlgebra over the non empty non void ManySortedSign is empty-yielding ; ::_thesis: verum end; end; begin definition let A be set ; func CatSign A -> strict ManySortedSign means :Def3: :: CATALG_1:def 3 ( the carrier of it = [:{0},(2 -tuples_on A):] & the carrier' of it = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of it . [1,<*a*>] = {} & the ResultSort of it . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of it . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of it . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ); existence ex b1 being strict ManySortedSign st ( the carrier of b1 = [:{0},(2 -tuples_on A):] & the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) proof defpred S1[ set , set ] means ex y1, y2, y3 being set st ( y1 in A & y2 in A & y3 in A & ( ( \$1 = [1,<*y1*>] & \$2 = [0,<*y1,y1*>] ) or ( \$1 = [2,<*y1,y2,y3*>] & \$2 = [0,<*y1,y3*>] ) ) ); defpred S2[ set , set ] means ex y1, y2, y3 being set st ( y1 in A & y2 in A & y3 in A & ( ( \$1 = [1,<*y1*>] & \$2 = {} ) or ( \$1 = [2,<*y1,y2,y3*>] & \$2 = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) ); A1: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds ex y being set st ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) proof let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies ex y being set st ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) ) assume A2: x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) percases ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by A2, XBOOLE_0:def_3; supposeA3: x in [:{1},(1 -tuples_on A):] ; ::_thesis: ex y being set st ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) then x `2 in 1 -tuples_on A by MCART_1:10; then A4: x `2 in { s where s is Element of A * : len s = 1 } by FINSEQ_2:def_4; take y = {} ; ::_thesis: ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) thus y in [:{0},(2 -tuples_on A):] * by FINSEQ_1:49; ::_thesis: S2[x,y] consider s being Element of A * such that A5: x `2 = s and A6: len s = 1 by A4; take y1 = s . 1; ::_thesis: ex y2, y3 being set st ( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) ) take y2 = s . 1; ::_thesis: ex y3 being set st ( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) ) take y3 = s . 1; ::_thesis: ( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) ) A7: s = <*y1*> by A6, FINSEQ_1:40; then ( y1 in {y1} & rng s = {y1} ) by FINSEQ_1:39, TARSKI:def_1; hence ( y1 in A & y2 in A & y3 in A ) ; ::_thesis: ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) x `1 in {1} by A3, MCART_1:10; then x `1 = 1 by TARSKI:def_1; hence ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) by A3, A5, A7, MCART_1:21; ::_thesis: verum end; supposeA8: x in [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) then x `2 in 3 -tuples_on A by MCART_1:10; then x `2 in { s where s is Element of A * : len s = 3 } by FINSEQ_2:def_4; then consider s being Element of A * such that A9: x `2 = s and A10: len s = 3 ; set y1 = s . 1; set y2 = s . 2; set y3 = s . 3; A11: s = <*(s . 1),(s . 2),(s . 3)*> by A10, FINSEQ_1:45; then A12: rng s = {(s . 1),(s . 2),(s . 3)} by FINSEQ_2:128; then reconsider B = A as non empty set ; take y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*>; ::_thesis: ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) A13: s . 2 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1; A14: s . 1 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1; then A15: ( 0 in {0} & <*(s . 1),(s . 2)*> in 2 -tuples_on B ) by A13, A12, FINSEQ_2:101, TARSKI:def_1; A16: s . 3 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1; then <*(s . 2),(s . 3)*> in 2 -tuples_on B by A13, A12, FINSEQ_2:101; then reconsider z1 = [0,<*(s . 2),(s . 3)*>], z2 = [0,<*(s . 1),(s . 2)*>] as Element of [:{0},(2 -tuples_on B):] by A15, ZFMISC_1:87; y = <*z1*> ^ <*z2*> by FINSEQ_1:def_9; hence y in [:{0},(2 -tuples_on A):] * by FINSEQ_1:def_11; ::_thesis: S2[x,y] take s . 1 ; ::_thesis: ex y2, y3 being set st ( s . 1 in A & y2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*(s . 1),y2*>]*> ) ) ) take s . 2 ; ::_thesis: ex y3 being set st ( s . 1 in A & s . 2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),y3*>] & y = <*[0,<*(s . 2),y3*>],[0,<*(s . 1),(s . 2)*>]*> ) ) ) take s . 3 ; ::_thesis: ( s . 1 in A & s . 2 in A & s . 3 in A & ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) ) ) thus ( s . 1 in A & s . 2 in A & s . 3 in A ) by A14, A13, A16, A12; ::_thesis: ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) ) x `1 in {2} by A8, MCART_1:10; then x `1 = 2 by TARSKI:def_1; hence ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) ) by A8, A9, A11, MCART_1:21; ::_thesis: verum end; end; end; consider Ar being Function such that A17: ( dom Ar = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & rng Ar c= [:{0},(2 -tuples_on A):] * ) and A18: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds S2[x,Ar . x] from FUNCT_1:sch_5(A1); reconsider Ar = Ar as Function of ([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),([:{0},(2 -tuples_on A):] *) by A17, FUNCT_2:2; A19: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds ex y being set st ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) proof let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies ex y being set st ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) ) assume A20: x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) percases ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by A20, XBOOLE_0:def_3; supposeA21: x in [:{1},(1 -tuples_on A):] ; ::_thesis: ex y being set st ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) then x `2 in 1 -tuples_on A by MCART_1:10; then x `2 in { s where s is Element of A * : len s = 1 } by FINSEQ_2:def_4; then consider s being Element of A * such that A22: x `2 = s and A23: len s = 1 ; set y1 = s . 1; set y2 = s . 1; set y3 = s . 1; A24: s = <*(s . 1)*> by A23, FINSEQ_1:40; then A25: ( s . 1 in {(s . 1)} & rng s = {(s . 1)} ) by FINSEQ_1:39, TARSKI:def_1; take y = [0,<*(s . 1),(s . 1)*>]; ::_thesis: ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) reconsider B = A as non empty set by A24; reconsider y1 = s . 1 as Element of B by A25; ( 0 in {0} & <*y1,y1*> in 2 -tuples_on B ) by FINSEQ_2:101, TARSKI:def_1; hence y in [:{0},(2 -tuples_on A):] by ZFMISC_1:87; ::_thesis: S1[x,y] take y1 ; ::_thesis: ex y2, y3 being set st ( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,y2,y3*>] & y = [0,<*y1,y3*>] ) ) ) take s . 1 ; ::_thesis: ex y3 being set st ( y1 in A & s . 1 in A & y3 in A & ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),y3*>] & y = [0,<*y1,y3*>] ) ) ) take s . 1 ; ::_thesis: ( y1 in A & s . 1 in A & s . 1 in A & ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) ) ) thus ( y1 in A & s . 1 in A & s . 1 in A ) by A25; ::_thesis: ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) ) x `1 in {1} by A21, MCART_1:10; then x `1 = 1 by TARSKI:def_1; hence ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) ) by A21, A22, A24, MCART_1:21; ::_thesis: verum end; supposeA26: x in [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) then x `2 in 3 -tuples_on A by MCART_1:10; then x `2 in { s where s is Element of A * : len s = 3 } by FINSEQ_2:def_4; then consider s being Element of A * such that A27: x `2 = s and A28: len s = 3 ; set y1 = s . 1; set y2 = s . 2; set y3 = s . 3; A29: s = <*(s . 1),(s . 2),(s . 3)*> by A28, FINSEQ_1:45; then A30: rng s = {(s . 1),(s . 2),(s . 3)} by FINSEQ_2:128; then reconsider B = A as non empty set ; take y = [0,<*(s . 1),(s . 3)*>]; ::_thesis: ( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) A31: ( s . 1 in {(s . 1),(s . 2),(s . 3)} & s . 3 in {(s . 1),(s . 2),(s . 3)} ) by ENUMSET1:def_1; then ( 0 in {0} & <*(s . 1),(s . 3)*> in 2 -tuples_on B ) by A30, FINSEQ_2:101, TARSKI:def_1; hence y in [:{0},(2 -tuples_on A):] by ZFMISC_1:87; ::_thesis: S1[x,y] take s . 1 ; ::_thesis: ex y2, y3 being set st ( s . 1 in A & y2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),y2,y3*>] & y = [0,<*(s . 1),y3*>] ) ) ) take s . 2 ; ::_thesis: ex y3 being set st ( s . 1 in A & s . 2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),y3*>] & y = [0,<*(s . 1),y3*>] ) ) ) take s . 3 ; ::_thesis: ( s . 1 in A & s . 2 in A & s . 3 in A & ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) ) ) s . 2 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1; hence ( s . 1 in A & s . 2 in A & s . 3 in A ) by A31, A30; ::_thesis: ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) ) x `1 in {2} by A26, MCART_1:10; then x `1 = 2 by TARSKI:def_1; hence ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) ) by A26, A27, A29, MCART_1:21; ::_thesis: verum end; end; end; consider R being Function such that A32: ( dom R = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & rng R c= [:{0},(2 -tuples_on A):] ) and A33: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds S1[x,R . x] from FUNCT_1:sch_5(A19); reconsider R = R as Function of ([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),[:{0},(2 -tuples_on A):] by A32, FUNCT_2:2; take S = ManySortedSign(# [:{0},(2 -tuples_on A):],([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),Ar,R #); ::_thesis: ( the carrier of S = [:{0},(2 -tuples_on A):] & the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) thus the carrier of S = [:{0},(2 -tuples_on A):] ; ::_thesis: ( the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) thus the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: ( ( for a being set st a in A holds ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) hereby ::_thesis: for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) let a be set ; ::_thesis: ( a in A implies ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] ) ) assume A34: a in A ; ::_thesis: ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] ) then reconsider B = A as non empty set ; reconsider x = a as Element of B by A34; ( <*x*> is Element of 1 -tuples_on B & 1 in {1} ) by FINSEQ_2:98, TARSKI:def_1; then [1,<*a*>] in [:{1},(1 -tuples_on A):] by ZFMISC_1:87; then A35: [1,<*a*>] in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by XBOOLE_0:def_3; then consider y1, y2, y3 being set such that y1 in A and y2 in A and y3 in A and A36: ( ( [1,<*a*>] = [1,<*y1*>] & R . [1,<*a*>] = [0,<*y1,y1*>] ) or ( [1,<*a*>] = [2,<*y1,y2,y3*>] & R . [1,<*a*>] = [0,<*y1,y3*>] ) ) by A33; ex y1, y2, y3 being set st ( y1 in A & y2 in A & y3 in A & ( ( [1,<*a*>] = [1,<*y1*>] & Ar . [1,<*a*>] = {} ) or ( [1,<*a*>] = [2,<*y1,y2,y3*>] & Ar . [1,<*a*>] = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) ) by A18, A35; hence the Arity of S . [1,<*a*>] = {} by XTUPLE_0:1; ::_thesis: the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] A37: ( <*a*> . 1 = a & <*y1*> . 1 = y1 ) by FINSEQ_1:40; <*a*> = <*y1*> by A36, XTUPLE_0:1; hence the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] by A36, A37, XTUPLE_0:1; ::_thesis: verum end; let a, b, c be set ; ::_thesis: ( a in A & b in A & c in A implies ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) assume that A38: a in A and A39: ( b in A & c in A ) ; ::_thesis: ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) reconsider B = A as non empty set by A38; reconsider x = a, y = b, z = c as Element of B by A38, A39; ( <*x,y,z*> is Element of 3 -tuples_on B & 2 in {2} ) by FINSEQ_2:104, TARSKI:def_1; then [2,<*a,b,c*>] in [:{2},(3 -tuples_on A):] by ZFMISC_1:87; then A40: [2,<*a,b,c*>] in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by XBOOLE_0:def_3; then consider y1, y2, y3 being set such that y1 in A and y2 in A and y3 in A and A41: ( ( [2,<*a,b,c*>] = [1,<*y1*>] & Ar . [2,<*a,b,c*>] = {} ) or ( [2,<*a,b,c*>] = [2,<*y1,y2,y3*>] & Ar . [2,<*a,b,c*>] = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) by A18; A42: ( <*a,b,c*> = (<*a*> ^ <*b*>) ^ <*c*> & <*y1,y2,y3*> = (<*y1*> ^ <*y2*>) ^ <*y3*> ) by FINSEQ_1:def_10; A43: <*a,b,c*> = <*y1,y2,y3*> by A41, XTUPLE_0:1; then A44: <*a*> ^ <*b*> = <*y1*> ^ <*y2*> by A42, FINSEQ_2:17; then <*a*> = <*y1*> by FINSEQ_2:17; then A45: a = y1 by Lm1; b = y2 by A44, FINSEQ_2:17; hence the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A41, A43, A42, A45, FINSEQ_2:17, XTUPLE_0:1; ::_thesis: the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] consider y1, y2, y3 being set such that y1 in A and y2 in A and y3 in A and A46: ( ( [2,<*a,b,c*>] = [1,<*y1*>] & R . [2,<*a,b,c*>] = [0,<*y1,y1*>] ) or ( [2,<*a,b,c*>] = [2,<*y1,y2,y3*>] & R . [2,<*a,b,c*>] = [0,<*y1,y3*>] ) ) by A33, A40; A47: ( <*a,b,c*> . 1 = a & <*y1,y2,y3*> . 1 = y1 ) by FINSEQ_1:45; A48: <*a,b,c*> . 3 = c by FINSEQ_1:45; <*a,b,c*> = <*y1,y2,y3*> by A46, XTUPLE_0:1; hence the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] by A46, A47, A48, FINSEQ_1:45, XTUPLE_0:1; ::_thesis: verum end; correctness uniqueness for b1, b2 being strict ManySortedSign st the carrier of b1 = [:{0},(2 -tuples_on A):] & the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) & the carrier of b2 = [:{0},(2 -tuples_on A):] & the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) holds b1 = b2; proof let S1, S2 be strict ManySortedSign ; ::_thesis: ( the carrier of S1 = [:{0},(2 -tuples_on A):] & the carrier' of S1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of S1 . [1,<*a*>] = {} & the ResultSort of S1 . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) & the carrier of S2 = [:{0},(2 -tuples_on A):] & the carrier' of S2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of S2 . [1,<*a*>] = {} & the ResultSort of S2 . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) implies S1 = S2 ) assume that A49: the carrier of S1 = [:{0},(2 -tuples_on A):] and A50: the carrier' of S1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and A51: for a being set st a in A holds ( the Arity of S1 . [1,<*a*>] = {} & the ResultSort of S1 . [1,<*a*>] = [0,<*a,a*>] ) and A52: for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) and A53: the carrier of S2 = [:{0},(2 -tuples_on A):] and A54: the carrier' of S2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and A55: for a being set st a in A holds ( the Arity of S2 . [1,<*a*>] = {} & the ResultSort of S2 . [1,<*a*>] = [0,<*a,a*>] ) and A56: for a, b, c being set st a in A & b in A & c in A holds ( the Arity of S2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ; ::_thesis: S1 = S2 A57: now__::_thesis:_for_x_being_set_st_x_in_[:{1},(1_-tuples_on_A):]_\/_[:{2},(3_-tuples_on_A):]_holds_ the_Arity_of_S1_._x_=_the_Arity_of_S2_._x let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies the Arity of S1 . x = the Arity of S2 . x ) assume x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: the Arity of S1 . x = the Arity of S2 . x then A58: ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def_3; then ( ( x `1 in {1} & x `2 in 1 -tuples_on A ) or ( x `1 in {2} & x `2 in 3 -tuples_on A ) ) by MCART_1:10; then A59: ( ( x `1 = 1 & x `2 in 1 -tuples_on A ) or ( x `1 = 2 & x `2 in 3 -tuples_on A ) ) by TARSKI:def_1; A60: now__::_thesis:_(_x_`2_in_3_-tuples_on_A_implies_the_Arity_of_S1_._[2,(x_`2)]_=_the_Arity_of_S2_._[2,(x_`2)]_) assume x `2 in 3 -tuples_on A ; ::_thesis: the Arity of S1 . [2,(x `2)] = the Arity of S2 . [2,(x `2)] then consider a, b, c being set such that A61: ( a in A & b in A & c in A & x `2 = <*a,b,c*> ) by FINSEQ_2:139; thus the Arity of S1 . [2,(x `2)] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A52, A61 .= the Arity of S2 . [2,(x `2)] by A56, A61 ; ::_thesis: verum end; A62: now__::_thesis:_(_x_`2_in_1_-tuples_on_A_implies_the_Arity_of_S1_._[1,(x_`2)]_=_the_Arity_of_S2_._[1,(x_`2)]_) assume x `2 in 1 -tuples_on A ; ::_thesis: the Arity of S1 . [1,(x `2)] = the Arity of S2 . [1,(x `2)] then A63: ex a being set st ( a in A & x `2 = <*a*> ) by FINSEQ_2:135; hence the Arity of S1 . [1,(x `2)] = {} by A51 .= the Arity of S2 . [1,(x `2)] by A55, A63 ; ::_thesis: verum end; x = [(x `1),(x `2)] by A58, MCART_1:21; hence the Arity of S1 . x = the Arity of S2 . x by A59, A62, A60; ::_thesis: verum end; A64: now__::_thesis:_for_x_being_set_st_x_in_[:{1},(1_-tuples_on_A):]_\/_[:{2},(3_-tuples_on_A):]_holds_ the_ResultSort_of_S1_._x_=_the_ResultSort_of_S2_._x let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies the ResultSort of S1 . x = the ResultSort of S2 . x ) assume x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: the ResultSort of S1 . x = the ResultSort of S2 . x then A65: ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def_3; then ( ( x `1 in {1} & x `2 in 1 -tuples_on A ) or ( x `1 in {2} & x `2 in 3 -tuples_on A ) ) by MCART_1:10; then A66: ( ( x `1 = 1 & x `2 in 1 -tuples_on A ) or ( x `1 = 2 & x `2 in 3 -tuples_on A ) ) by TARSKI:def_1; A67: now__::_thesis:_(_x_`2_in_3_-tuples_on_A_implies_the_ResultSort_of_S1_._[2,(x_`2)]_=_the_ResultSort_of_S2_._[2,(x_`2)]_) assume x `2 in 3 -tuples_on A ; ::_thesis: the ResultSort of S1 . [2,(x `2)] = the ResultSort of S2 . [2,(x `2)] then consider a, b, c being set such that A68: ( a in A & b in A & c in A & x `2 = <*a,b,c*> ) by FINSEQ_2:139; thus the ResultSort of S1 . [2,(x `2)] = [0,<*a,c*>] by A52, A68 .= the ResultSort of S2 . [2,(x `2)] by A56, A68 ; ::_thesis: verum end; A69: now__::_thesis:_(_x_`2_in_1_-tuples_on_A_implies_the_ResultSort_of_S1_._[1,(x_`2)]_=_the_ResultSort_of_S2_._[1,(x_`2)]_) assume x `2 in 1 -tuples_on A ; ::_thesis: the ResultSort of S1 . [1,(x `2)] = the ResultSort of S2 . [1,(x `2)] then consider a being set such that A70: ( a in A & x `2 = <*a*> ) by FINSEQ_2:135; thus the ResultSort of S1 . [1,(x `2)] = [0,<*a,a*>] by A51, A70 .= the ResultSort of S2 . [1,(x `2)] by A55, A70 ; ::_thesis: verum end; x = [(x `1),(x `2)] by A65, MCART_1:21; hence the ResultSort of S1 . x = the ResultSort of S2 . x by A66, A69, A67; ::_thesis: verum end; ( dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the carrier' of S2 ) by FUNCT_2:def_1; then A71: the Arity of S1 = the Arity of S2 by A50, A54, A57, FUNCT_1:2; now__::_thesis:_(_[:{0},(2_-tuples_on_A):]_=_{}_implies_[:{1},(1_-tuples_on_A):]_\/_[:{2},(3_-tuples_on_A):]_=_{}_) assume [:{0},(2 -tuples_on A):] = {} ; ::_thesis: [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} then A = {} ; then A72: ( 1 <> 0 & 3 <> 0 implies ( 1 -tuples_on A = {} & 3 -tuples_on A = {} ) ) by FINSEQ_3:119; then [:{1},(1 -tuples_on A):] = {} by ZFMISC_1:90; hence [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} by A72, ZFMISC_1:90; ::_thesis: verum end; then ( dom the ResultSort of S1 = the carrier' of S1 & dom the ResultSort of S2 = the carrier' of S2 ) by A49, A50, A53, A54, FUNCT_2:def_1; hence S1 = S2 by A49, A50, A53, A54, A71, A64, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines CatSign CATALG_1:def_3_:_ for A being set for b2 being strict ManySortedSign holds ( b2 = CatSign A iff ( the carrier of b2 = [:{0},(2 -tuples_on A):] & the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds ( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds ( the Arity of b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) ); registration let A be set ; cluster CatSign A -> strict feasible ; coherence CatSign A is feasible proof assume the carrier of (CatSign A) = {} ; :: according to INSTALG1:def_1 ::_thesis: the carrier' of (CatSign A) = {} then [:{0},(2 -tuples_on A):] = {} by Def3; then A = {} ; then A1: ( 1 <> 0 & 3 <> 0 implies ( 1 -tuples_on A = {} & 3 -tuples_on A = {} ) ) by FINSEQ_3:119; then [:{1},(1 -tuples_on A):] = {} by ZFMISC_1:90; then [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} by A1, ZFMISC_1:90; hence the carrier' of (CatSign A) = {} by Def3; ::_thesis: verum end; end; registration let A be non empty set ; cluster CatSign A -> non empty non void strict ; coherence ( not CatSign A is empty & not CatSign A is void ) proof the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3; hence not the carrier of (CatSign A) is empty ; :: according to STRUCT_0:def_1 ::_thesis: not CatSign A is void the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; hence not the carrier' of (CatSign A) is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum end; end; definition mode Signature is feasible ManySortedSign ; end; definition let S be Signature; attrS is Categorial means :Def4: :: CATALG_1:def 4 ex A being set st ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ); end; :: deftheorem Def4 defines Categorial CATALG_1:def_4_:_ for S being Signature holds ( S is Categorial iff ex A being set st ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) ); registration cluster non empty feasible Categorial -> non empty non void for ManySortedSign ; coherence for b1 being non empty Signature st b1 is Categorial holds not b1 is void proof let S be non empty Signature; ::_thesis: ( S is Categorial implies not S is void ) given A being set such that A1: CatSign A is Subsignature of S and A2: the carrier of S = [:{0},(2 -tuples_on A):] ; :: according to CATALG_1:def_4 ::_thesis: not S is void set s = the SortSymbol of S; consider z, p being set such that z in {0} and A3: p in 2 -tuples_on A and the SortSymbol of S = [z,p] by A2, ZFMISC_1:84; 2 -tuples_on A = { q where q is Element of A * : len q = 2 } by FINSEQ_2:def_4; then consider q being Element of A * such that p = q and A4: len q = 2 by A3; A5: dom q = Seg 2 by A4, FINSEQ_1:def_3; then reconsider A9 = A as non empty set ; 1 in dom q by A5, FINSEQ_1:2, TARSKI:def_2; then q . 1 in rng q by FUNCT_1:def_3; then reconsider a = q . 1 as Element of A9 ; the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; then ( <*a*> is Element of 1 -tuples_on A9 & [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] c= the carrier' of S ) by A1, FINSEQ_2:98, INSTALG1:10; hence not the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum end; end; registration cluster non empty strict feasible Categorial for ManySortedSign ; existence ex b1 being Signature st ( b1 is Categorial & not b1 is empty & b1 is strict ) proof take S = CatSign {{}}; ::_thesis: ( S is Categorial & not S is empty & S is strict ) thus S is Categorial ::_thesis: ( not S is empty & S is strict ) proof take {{}} ; :: according to CATALG_1:def_4 ::_thesis: ( CatSign {{}} is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on {{}}):] ) thus ( CatSign {{}} is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on {{}}):] ) by Def3, INSTALG1:15; ::_thesis: verum end; thus ( not S is empty & S is strict ) ; ::_thesis: verum end; end; definition mode CatSignature is Categorial Signature; end; definition let A be set ; mode CatSignature of A -> Signature means :Def5: :: CATALG_1:def 5 ( CatSign A is Subsignature of it & the carrier of it = [:{0},(2 -tuples_on A):] ); existence ex b1 being Signature st ( CatSign A is Subsignature of b1 & the carrier of b1 = [:{0},(2 -tuples_on A):] ) proof set S = CatSign A; ( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15; then reconsider S = CatSign A as CatSignature by Def4; take S ; ::_thesis: ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) thus ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15; ::_thesis: verum end; end; :: deftheorem Def5 defines CatSignature CATALG_1:def_5_:_ for A being set for b2 being Signature holds ( b2 is CatSignature of A iff ( CatSign A is Subsignature of b2 & the carrier of b2 = [:{0},(2 -tuples_on A):] ) ); theorem :: CATALG_1:4 for A1, A2 being set for S being CatSignature of A1 st S is CatSignature of A2 holds A1 = A2 proof let A1, A2 be set ; ::_thesis: for S being CatSignature of A1 st S is CatSignature of A2 holds A1 = A2 let S be CatSignature of A1; ::_thesis: ( S is CatSignature of A2 implies A1 = A2 ) assume that CatSign A2 is Subsignature of S and A1: the carrier of S = [:{0},(2 -tuples_on A2):] ; :: according to CATALG_1:def_5 ::_thesis: A1 = A2 A2: [:{0},(2 -tuples_on A1):] = [:{0},(2 -tuples_on A2):] by A1, Def5; then A3: 2 -tuples_on A1 c= 2 -tuples_on A2 by ZFMISC_1:94; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A2 c= A1 let x be set ; ::_thesis: ( x in A1 implies x in A2 ) assume x in A1 ; ::_thesis: x in A2 then <*x,x*> in 2 -tuples_on A1 by FINSEQ_2:137; hence x in A2 by A3, FINSEQ_2:138; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A2 or x in A1 ) assume x in A2 ; ::_thesis: x in A1 then A4: <*x,x*> in 2 -tuples_on A2 by FINSEQ_2:137; 2 -tuples_on A2 c= 2 -tuples_on A1 by A2, ZFMISC_1:94; hence x in A1 by A4, FINSEQ_2:138; ::_thesis: verum end; registration let A be set ; cluster -> Categorial for CatSignature of A; coherence for b1 being CatSignature of A holds b1 is Categorial proof let S be CatSignature of A; ::_thesis: S is Categorial take A ; :: according to CATALG_1:def_4 ::_thesis: ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) thus ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) by Def5; ::_thesis: verum end; end; registration let A be non empty set ; cluster -> non empty for CatSignature of A; coherence for b1 being CatSignature of A holds not b1 is empty proof let S be CatSignature of A; ::_thesis: not S is empty CatSign A is Subsignature of S by Def5; then the carrier of (CatSign A) c= the carrier of S by INSTALG1:10; hence not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; registration let A be set ; cluster strict feasible Categorial for CatSignature of A; existence ex b1 being CatSignature of A st b1 is strict proof set S = CatSign A; ( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15; then CatSign A is CatSignature of A by Def5; hence ex b1 being CatSignature of A st b1 is strict ; ::_thesis: verum end; end; definition let A be set ; :: original: CatSign redefine func CatSign A -> strict CatSignature of A; coherence CatSign A is strict CatSignature of A proof set S = CatSign A; ( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15; hence CatSign A is strict CatSignature of A by Def5; ::_thesis: verum end; end; definition let S be ManySortedSign ; func underlay S -> set means :Def6: :: CATALG_1:def 6 for x being set holds ( x in it iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) proof set A = the carrier of S \/ the carrier' of S; take X = proj2 (union (SubFuncs (proj2 ( the carrier of S \/ the carrier' of S)))); ::_thesis: for x being set holds ( x in X iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) let x be set ; ::_thesis: ( x in X iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) hereby ::_thesis: ( ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) implies x in X ) assume x in X ; ::_thesis: ex c being set ex b being Function st ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b ) then consider a being set such that A1: [a,x] in union (SubFuncs (proj2 ( the carrier of S \/ the carrier' of S))) by XTUPLE_0:def_13; consider b being set such that A2: [a,x] in b and A3: b in SubFuncs (proj2 ( the carrier of S \/ the carrier' of S)) by A1, TARSKI:def_4; reconsider b = b as Function by A3, FUNCT_6:def_1; b in proj2 ( the carrier of S \/ the carrier' of S) by A3, FUNCT_6:def_1; then consider c being set such that A4: [c,b] in the carrier of S \/ the carrier' of S by XTUPLE_0:def_13; take c = c; ::_thesis: ex b being Function st ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b ) take b = b; ::_thesis: ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b ) thus ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b ) by A2, A4, XTUPLE_0:def_13; ::_thesis: verum end; given a being set , f being Function such that A5: [a,f] in the carrier of S \/ the carrier' of S and A6: x in rng f ; ::_thesis: x in X consider b being set such that A7: [b,x] in f by A6, XTUPLE_0:def_13; f in proj2 ( the carrier of S \/ the carrier' of S) by A5, XTUPLE_0:def_13; then f in SubFuncs (proj2 ( the carrier of S \/ the carrier' of S)) by FUNCT_6:def_1; then [b,x] in union (SubFuncs (proj2 ( the carrier of S \/ the carrier' of S))) by A7, TARSKI:def_4; hence x in X by XTUPLE_0:def_13; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) & ( for x being set holds ( x in b2 iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & \$1 in rng f ); thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def6 defines underlay CATALG_1:def_6_:_ for S being ManySortedSign for b2 being set holds ( b2 = underlay S iff for x being set holds ( x in b2 iff ex a being set ex f being Function st ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ); theorem Th5: :: CATALG_1:5 for A being set holds underlay (CatSign A) = A proof let A be set ; ::_thesis: underlay (CatSign A) = A set S = CatSign A; A1: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= underlay (CatSign A) let x be set ; ::_thesis: ( x in underlay (CatSign A) implies x in A ) assume x in underlay (CatSign A) ; ::_thesis: x in A then consider a being set , f being Function such that A2: [a,f] in the carrier of (CatSign A) \/ the carrier' of (CatSign A) and A3: x in rng f by Def6; ( [a,f] in the carrier of (CatSign A) or [a,f] in the carrier' of (CatSign A) ) by A2, XBOOLE_0:def_3; then ( [a,f] in [:{0},(2 -tuples_on A):] or [a,f] in [:{1},(1 -tuples_on A):] or [a,f] in [:{2},(3 -tuples_on A):] ) by A1, Def3, XBOOLE_0:def_3; then ( f in 2 -tuples_on A or f in 1 -tuples_on A or f in 3 -tuples_on A ) by ZFMISC_1:87; then f is FinSequence of A by FINSEQ_2:def_3; then rng f c= A by FINSEQ_1:def_4; hence x in A by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in underlay (CatSign A) ) assume x in A ; ::_thesis: x in underlay (CatSign A) then A4: <*x,x*> in 2 -tuples_on A by FINSEQ_2:137; the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3; then [0,<*x,x*>] in the carrier of (CatSign A) by A4, ZFMISC_1:105; then A5: [0,<*x,x*>] in the carrier of (CatSign A) \/ the carrier' of (CatSign A) by XBOOLE_0:def_3; rng <*x,x*> = {x,x} by FINSEQ_2:127; then x in rng <*x,x*> by TARSKI:def_2; hence x in underlay (CatSign A) by A5, Def6; ::_thesis: verum end; definition let S be ManySortedSign ; attrS is delta-concrete means :Def7: :: CATALG_1:def 7 ex f being Function of NAT,NAT st ( ( for s being set st s in the carrier of S holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being set st o in the carrier' of S holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) ); end; :: deftheorem Def7 defines delta-concrete CATALG_1:def_7_:_ for S being ManySortedSign holds ( S is delta-concrete iff ex f being Function of NAT,NAT st ( ( for s being set st s in the carrier of S holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being set st o in the carrier' of S holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) ) ); registration let A be set ; cluster CatSign A -> strict delta-concrete ; coherence CatSign A is delta-concrete proof defpred S1[ set , set ] means ( ( A = 0 implies c2 = 2 ) & ( A = 1 implies c2 = 1 ) & ( A = 2 implies c2 = 3 ) ); set S = CatSign A; A1: for x being set st x in NAT holds ex y being set st ( y in NAT & S1[x,y] ) proof reconsider j0 = 2, j1 = 1, j2 = 3 as set ; let i be set ; ::_thesis: ( i in NAT implies ex y being set st ( y in NAT & S1[i,y] ) ) assume i in NAT ; ::_thesis: ex y being set st ( y in NAT & S1[i,y] ) percases ( i = 0 or i = 1 or i = 2 or ( i <> 0 & i <> 1 & i <> 2 ) ) ; supposeA2: i = 0 ; ::_thesis: ex y being set st ( y in NAT & S1[i,y] ) take j0 ; ::_thesis: ( j0 in NAT & S1[i,j0] ) thus ( j0 in NAT & S1[i,j0] ) by A2; ::_thesis: verum end; supposeA3: i = 1 ; ::_thesis: ex y being set st ( y in NAT & S1[i,y] ) take j1 ; ::_thesis: ( j1 in NAT & S1[i,j1] ) thus ( j1 in NAT & S1[i,j1] ) by A3; ::_thesis: verum end; supposeA4: i = 2 ; ::_thesis: ex y being set st ( y in NAT & S1[i,y] ) take j2 ; ::_thesis: ( j2 in NAT & S1[i,j2] ) thus ( j2 in NAT & S1[i,j2] ) by A4; ::_thesis: verum end; supposeA5: ( i <> 0 & i <> 1 & i <> 2 ) ; ::_thesis: ex y being set st ( y in NAT & S1[i,y] ) take j0 ; ::_thesis: ( j0 in NAT & S1[i,j0] ) thus ( j0 in NAT & S1[i,j0] ) by A5; ::_thesis: verum end; end; end; consider f being Function such that A6: ( dom f = NAT & rng f c= NAT ) and A7: for i being set st i in NAT holds S1[i,f . i] from FUNCT_1:sch_5(A1); reconsider f = f as Function of NAT,NAT by A6, FUNCT_2:2; take f ; :: according to CATALG_1:def_7 ::_thesis: ( ( for s being set st s in the carrier of (CatSign A) holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) ) & ( for o being set st o in the carrier' of (CatSign A) holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) ) ) A8: A = underlay (CatSign A) by Th5; A9: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3; hereby ::_thesis: for o being set st o in the carrier' of (CatSign A) holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) let s be set ; ::_thesis: ( s in the carrier of (CatSign A) implies ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) ) assume s in the carrier of (CatSign A) ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) then consider i, p being set such that A10: i in {0} and A11: p in 2 -tuples_on A and A12: s = [i,p] by A9, ZFMISC_1:84; reconsider p = p as FinSequence by A11; take i = 0 ; ::_thesis: ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) take p = p; ::_thesis: ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) f . i = 2 by A7; hence ( s = [i,p] & len p = f . i ) by A10, A11, A12, FINSEQ_2:132, TARSKI:def_1; ::_thesis: [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) thus [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) by A7, A9, A8; ::_thesis: verum end; let o be set ; ::_thesis: ( o in the carrier' of (CatSign A) implies ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) ) A13: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; assume A14: o in the carrier' of (CatSign A) ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) percases ( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] ) by A13, A14, XBOOLE_0:def_3; suppose o in [:{1},(1 -tuples_on A):] ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) then consider i, p being set such that A15: i in {1} and A16: p in 1 -tuples_on A and A17: o = [i,p] by ZFMISC_1:84; reconsider p = p as FinSequence of A by A16, FINSEQ_2:def_3; take i = 1; ::_thesis: ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) take p ; ::_thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) f . i = 1 by A7; hence ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) by A13, A8, A15, A16, A17, FINSEQ_2:132, TARSKI:def_1, XBOOLE_1:7; ::_thesis: verum end; suppose o in [:{2},(3 -tuples_on A):] ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) then consider i, p being set such that A18: i in {2} and A19: p in 3 -tuples_on A and A20: o = [i,p] by ZFMISC_1:84; reconsider p = p as FinSequence of A by A19, FINSEQ_2:def_3; take i = 2; ::_thesis: ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) take p ; ::_thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) f . i = 3 by A7; hence ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) by A13, A8, A18, A19, A20, FINSEQ_2:132, TARSKI:def_1, XBOOLE_1:7; ::_thesis: verum end; end; end; end; registration cluster non empty strict feasible Categorial delta-concrete for ManySortedSign ; existence ex b1 being CatSignature st ( b1 is delta-concrete & not b1 is empty & b1 is strict ) proof take CatSign {{}} ; ::_thesis: ( CatSign {{}} is delta-concrete & not CatSign {{}} is empty & CatSign {{}} is strict ) thus ( CatSign {{}} is delta-concrete & not CatSign {{}} is empty & CatSign {{}} is strict ) ; ::_thesis: verum end; let A be set ; cluster strict feasible Categorial delta-concrete for CatSignature of A; existence ex b1 being CatSignature of A st ( b1 is delta-concrete & b1 is strict ) proof take CatSign A ; ::_thesis: ( CatSign A is delta-concrete & CatSign A is strict ) thus ( CatSign A is delta-concrete & CatSign A is strict ) ; ::_thesis: verum end; end; theorem Th6: :: CATALG_1:6 for S being delta-concrete ManySortedSign for x being set st ( x in the carrier of S or x in the carrier' of S ) holds ex i being Element of NAT ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) proof let S be delta-concrete ManySortedSign ; ::_thesis: for x being set st ( x in the carrier of S or x in the carrier' of S ) holds ex i being Element of NAT ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) let x be set ; ::_thesis: ( ( x in the carrier of S or x in the carrier' of S ) implies ex i being Element of NAT ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) ) assume A1: ( x in the carrier of S or x in the carrier' of S ) ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) A2: x in the carrier of S \/ the carrier' of S by A1, XBOOLE_0:def_3; consider f being Function of NAT,NAT such that A3: for s being set st s in the carrier of S holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) and A4: for o being set st o in the carrier' of S holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) by Def7; percases ( x in the carrier of S or x in the carrier' of S ) by A1; suppose x in the carrier of S ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) then consider i being Element of NAT , p being FinSequence such that A5: x = [i,p] and len p = f . i and [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S by A3; take i ; ::_thesis: ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) take p ; ::_thesis: ( x = [i,p] & rng p c= underlay S ) thus x = [i,p] by A5; ::_thesis: rng p c= underlay S let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng p or a in underlay S ) thus ( not a in rng p or a in underlay S ) by A2, A5, Def6; ::_thesis: verum end; suppose x in the carrier' of S ; ::_thesis: ex i being Element of NAT ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) then consider i being Element of NAT , p being FinSequence such that A6: x = [i,p] and len p = f . i and [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S by A4; take i ; ::_thesis: ex p being FinSequence st ( x = [i,p] & rng p c= underlay S ) take p ; ::_thesis: ( x = [i,p] & rng p c= underlay S ) thus x = [i,p] by A6; ::_thesis: rng p c= underlay S let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng p or a in underlay S ) thus ( not a in rng p or a in underlay S ) by A2, A6, Def6; ::_thesis: verum end; end; end; theorem :: CATALG_1:7 for S being delta-concrete ManySortedSign for i being set for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds len p1 = len p2 proof let S be delta-concrete ManySortedSign ; ::_thesis: for i being set for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds len p1 = len p2 let i be set ; ::_thesis: for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds len p1 = len p2 let p1, p2 be FinSequence; ::_thesis: ( ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) implies len p1 = len p2 ) assume A1: ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) ; ::_thesis: len p1 = len p2 consider f being Function of NAT,NAT such that A2: for s being set st s in the carrier of S holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) and A3: for o being set st o in the carrier' of S holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) by Def7; percases ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) by A1; supposeA4: ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) ; ::_thesis: len p1 = len p2 then consider j1 being Element of NAT , q1 being FinSequence such that A5: [i,p1] = [j1,q1] and A6: len q1 = f . j1 and [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier of S by A2; A7: ( i = j1 & p1 = q1 ) by A5, XTUPLE_0:1; consider j2 being Element of NAT , q2 being FinSequence such that A8: [i,p2] = [j2,q2] and A9: len q2 = f . j2 and [:{j2},((f . j2) -tuples_on (underlay S)):] c= the carrier of S by A2, A4; i = j2 by A8, XTUPLE_0:1; hence len p1 = len p2 by A6, A8, A9, A7, XTUPLE_0:1; ::_thesis: verum end; supposeA10: ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ; ::_thesis: len p1 = len p2 then consider j1 being Element of NAT , q1 being FinSequence such that A11: [i,p1] = [j1,q1] and A12: len q1 = f . j1 and [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier' of S by A3; A13: ( i = j1 & p1 = q1 ) by A11, XTUPLE_0:1; consider j2 being Element of NAT , q2 being FinSequence such that A14: [i,p2] = [j2,q2] and A15: len q2 = f . j2 and [:{j2},((f . j2) -tuples_on (underlay S)):] c= the carrier' of S by A3, A10; i = j2 by A14, XTUPLE_0:1; hence len p1 = len p2 by A12, A14, A15, A13, XTUPLE_0:1; ::_thesis: verum end; end; end; theorem :: CATALG_1:8 for S being delta-concrete ManySortedSign for i being set for p1, p2 being FinSequence st len p2 = len p1 & rng p2 c= underlay S holds ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) ) proof let S be delta-concrete ManySortedSign ; ::_thesis: for i being set for p1, p2 being FinSequence st len p2 = len p1 & rng p2 c= underlay S holds ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) ) let i be set ; ::_thesis: for p1, p2 being FinSequence st len p2 = len p1 & rng p2 c= underlay S holds ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) ) let p1, p2 be FinSequence; ::_thesis: ( len p2 = len p1 & rng p2 c= underlay S implies ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) ) ) assume A1: ( len p2 = len p1 & rng p2 c= underlay S ) ; ::_thesis: ( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) ) consider f being Function of NAT,NAT such that A2: for s being set st s in the carrier of S holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) and A3: for o being set st o in the carrier' of S holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) by Def7; hereby ::_thesis: ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) assume [i,p1] in the carrier of S ; ::_thesis: [i,p2] in the carrier of S then consider j1 being Element of NAT , q1 being FinSequence such that A4: [i,p1] = [j1,q1] and A5: len q1 = f . j1 and A6: [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier of S by A2; p1 = q1 by A4, XTUPLE_0:1; then A7: p2 in (f . j1) -tuples_on (underlay S) by A1, A5, FINSEQ_2:132; i = j1 by A4, XTUPLE_0:1; then [i,p2] in [:{j1},((f . j1) -tuples_on (underlay S)):] by A7, ZFMISC_1:105; hence [i,p2] in the carrier of S by A6; ::_thesis: verum end; assume [i,p1] in the carrier' of S ; ::_thesis: [i,p2] in the carrier' of S then consider j1 being Element of NAT , q1 being FinSequence such that A8: [i,p1] = [j1,q1] and A9: len q1 = f . j1 and A10: [:{j1},((f . j1) -tuples_on (underlay S)):] c= the carrier' of S by A3; p1 = q1 by A8, XTUPLE_0:1; then A11: p2 in (f . j1) -tuples_on (underlay S) by A1, A9, FINSEQ_2:132; i = j1 by A8, XTUPLE_0:1; then [i,p2] in [:{j1},((f . j1) -tuples_on (underlay S)):] by A11, ZFMISC_1:105; hence [i,p2] in the carrier' of S by A10; ::_thesis: verum end; theorem :: CATALG_1:9 for S being non empty Categorial delta-concrete Signature holds S is CatSignature of underlay S proof let S be non empty Categorial delta-concrete Signature; ::_thesis: S is CatSignature of underlay S set s = the SortSymbol of S; consider A being set such that A1: CatSign A is Subsignature of S and A2: the carrier of S = [:{0},(2 -tuples_on A):] by Def4; consider f being Function of NAT,NAT such that A3: for s being set st s in the carrier of S holds ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) and for o being set st o in the carrier' of S holds ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) by Def7; consider i being Element of NAT , p being FinSequence such that A4: the SortSymbol of S = [i,p] and A5: ( len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) by A3; p in 2 -tuples_on A by A2, A4, ZFMISC_1:105; then A6: len p = 2 by FINSEQ_2:132; A7: A c= underlay S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in underlay S ) assume x in A ; ::_thesis: x in underlay S then <*x,x*> in 2 -tuples_on A by FINSEQ_2:137; then [0,<*x,x*>] in the carrier of S by A2, ZFMISC_1:105; then A8: [0,<*x,x*>] in the carrier of S \/ the carrier' of S by XBOOLE_0:def_3; rng <*x,x*> = {x,x} by FINSEQ_2:127; then x in rng <*x,x*> by TARSKI:def_2; hence x in underlay S by A8, Def6; ::_thesis: verum end; i = 0 by A2, A4, ZFMISC_1:105; then A9: 2 -tuples_on (underlay S) c= 2 -tuples_on A by A2, A5, A6, ZFMISC_1:94; underlay S c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in underlay S or x in A ) assume x in underlay S ; ::_thesis: x in A then <*x,x*> in 2 -tuples_on (underlay S) by FINSEQ_2:137; hence x in A by A9, FINSEQ_2:138; ::_thesis: verum end; then A = underlay S by A7, XBOOLE_0:def_10; hence S is CatSignature of underlay S by A1, A2, Def5; ::_thesis: verum end; begin registration let S be non empty CatSignature; let s be SortSymbol of S; clusters `2 -> Relation-like Function-like ; coherence ( s `2 is Relation-like & s `2 is Function-like ) proof consider A being set such that CatSign A is Subsignature of S and A1: the carrier of S = [:{0},(2 -tuples_on A):] by Def4; s `2 in 2 -tuples_on A by A1, MCART_1:10; hence ( s `2 is Relation-like & s `2 is Function-like ) ; ::_thesis: verum end; end; registration let S be non empty delta-concrete ManySortedSign ; let s be SortSymbol of S; clusters `2 -> Relation-like Function-like ; coherence ( s `2 is Relation-like & s `2 is Function-like ) proof ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & rng p c= underlay S ) by Th6; hence ( s `2 is Relation-like & s `2 is Function-like ) by MCART_1:7; ::_thesis: verum end; end; registration let S be non void delta-concrete ManySortedSign ; let o be Element of the carrier' of S; clustero `2 -> Relation-like Function-like ; coherence ( o `2 is Relation-like & o `2 is Function-like ) proof ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & rng p c= underlay S ) by Th6; hence ( o `2 is Relation-like & o `2 is Function-like ) by MCART_1:7; ::_thesis: verum end; end; registration let S be non empty CatSignature; let s be SortSymbol of S; clusters `2 -> FinSequence-like ; coherence s `2 is FinSequence-like proof consider A being set such that CatSign A is Subsignature of S and A1: the carrier of S = [:{0},(2 -tuples_on A):] by Def4; s `2 in 2 -tuples_on A by A1, MCART_1:10; then ex a, b being set st ( a in A & b in A & s `2 = <*a,b*> ) by FINSEQ_2:137; hence s `2 is FinSequence-like ; ::_thesis: verum end; end; registration let S be non empty delta-concrete ManySortedSign ; let s be SortSymbol of S; clusters `2 -> FinSequence-like ; coherence s `2 is FinSequence-like proof ex i being Element of NAT ex p being FinSequence st ( s = [i,p] & rng p c= underlay S ) by Th6; hence s `2 is FinSequence-like by MCART_1:7; ::_thesis: verum end; end; registration let S be non void delta-concrete ManySortedSign ; let o be Element of the carrier' of S; clustero `2 -> FinSequence-like ; coherence o `2 is FinSequence-like proof ex i being Element of NAT ex p being FinSequence st ( o = [i,p] & rng p c= underlay S ) by Th6; hence o `2 is FinSequence-like by MCART_1:7; ::_thesis: verum end; end; definition let a be set ; func idsym a -> set equals :: CATALG_1:def 8 [1,<*a*>]; correctness coherence [1,<*a*>] is set ; ; let b be set ; func homsym (a,b) -> set equals :: CATALG_1:def 9 [0,<*a,b*>]; correctness coherence [0,<*a,b*>] is set ; ; let c be set ; func compsym (a,b,c) -> set equals :: CATALG_1:def 10 [2,<*a,b,c*>]; correctness coherence [2,<*a,b,c*>] is set ; ; end; :: deftheorem defines idsym CATALG_1:def_8_:_ for a being set holds idsym a = [1,<*a*>]; :: deftheorem defines homsym CATALG_1:def_9_:_ for a, b being set holds homsym (a,b) = [0,<*a,b*>]; :: deftheorem defines compsym CATALG_1:def_10_:_ for a, b, c being set holds compsym (a,b,c) = [2,<*a,b,c*>]; theorem Th10: :: CATALG_1:10 for A being non empty set for S being CatSignature of A for a being Element of A holds ( idsym a in the carrier' of S & ( for b being Element of A holds ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) ) proof let A be non empty set ; ::_thesis: for S being CatSignature of A for a being Element of A holds ( idsym a in the carrier' of S & ( for b being Element of A holds ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) ) let S be CatSignature of A; ::_thesis: for a being Element of A holds ( idsym a in the carrier' of S & ( for b being Element of A holds ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) ) let a be Element of A; ::_thesis: ( idsym a in the carrier' of S & ( for b being Element of A holds ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) ) A1: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; A2: CatSign A is Subsignature of S by Def5; then A3: the carrier of (CatSign A) c= the carrier of S by INSTALG1:10; A4: the carrier' of (CatSign A) c= the carrier' of S by A2, INSTALG1:10; <*a*> in 1 -tuples_on A by FINSEQ_2:135; then [1,<*a*>] in [:{1},(1 -tuples_on A):] by ZFMISC_1:105; then [1,<*a*>] in the carrier' of (CatSign A) by A1, XBOOLE_0:def_3; hence idsym a in the carrier' of S by A4; ::_thesis: for b being Element of A holds ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) let b be Element of A; ::_thesis: ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) A5: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3; <*a,b*> in 2 -tuples_on A by FINSEQ_2:137; then [0,<*a,b*>] in [:{0},(2 -tuples_on A):] by ZFMISC_1:105; hence homsym (a,b) in the carrier of S by A3, A5; ::_thesis: for c being Element of A holds compsym (a,b,c) in the carrier' of S let c be Element of A; ::_thesis: compsym (a,b,c) in the carrier' of S <*a,b,c*> in 3 -tuples_on A by FINSEQ_2:139; then [2,<*a,b,c*>] in [:{2},(3 -tuples_on A):] by ZFMISC_1:105; then [2,<*a,b,c*>] in the carrier' of (CatSign A) by A1, XBOOLE_0:def_3; hence compsym (a,b,c) in the carrier' of S by A4; ::_thesis: verum end; definition let A be non empty set ; let a be Element of A; :: original: idsym redefine func idsym a -> OperSymbol of (CatSign A); correctness coherence idsym a is OperSymbol of (CatSign A); by Th10; let b be Element of A; :: original: homsym redefine func homsym (a,b) -> SortSymbol of (CatSign A); correctness coherence homsym (a,b) is SortSymbol of (CatSign A); by Th10; let c be Element of A; :: original: compsym redefine func compsym (a,b,c) -> OperSymbol of (CatSign A); correctness coherence compsym (a,b,c) is OperSymbol of (CatSign A); by Th10; end; theorem Th11: :: CATALG_1:11 for a, b being set st idsym a = idsym b holds a = b proof let a, b be set ; ::_thesis: ( idsym a = idsym b implies a = b ) assume idsym a = idsym b ; ::_thesis: a = b then <*a*> = <*b*> by XTUPLE_0:1; hence a = b by Lm1; ::_thesis: verum end; theorem Th12: :: CATALG_1:12 for a1, b1, a2, b2 being set st homsym (a1,a2) = homsym (b1,b2) holds ( a1 = b1 & a2 = b2 ) proof let a1, b1, a2, b2 be set ; ::_thesis: ( homsym (a1,a2) = homsym (b1,b2) implies ( a1 = b1 & a2 = b2 ) ) assume homsym (a1,a2) = homsym (b1,b2) ; ::_thesis: ( a1 = b1 & a2 = b2 ) then A1: <*a1,a2*> = <*b1,b2*> by XTUPLE_0:1; ( <*a1,a2*> . 1 = a1 & <*a1,a2*> . 2 = a2 ) by FINSEQ_1:44; hence ( a1 = b1 & a2 = b2 ) by A1, FINSEQ_1:44; ::_thesis: verum end; theorem Th13: :: CATALG_1:13 for a1, b1, a2, b2, a3, b3 being set st compsym (a1,a2,a3) = compsym (b1,b2,b3) holds ( a1 = b1 & a2 = b2 & a3 = b3 ) proof let a1, b1, a2, b2, a3, b3 be set ; ::_thesis: ( compsym (a1,a2,a3) = compsym (b1,b2,b3) implies ( a1 = b1 & a2 = b2 & a3 = b3 ) ) A1: <*a1,a2,a3*> . 3 = a3 by FINSEQ_1:45; assume compsym (a1,a2,a3) = compsym (b1,b2,b3) ; ::_thesis: ( a1 = b1 & a2 = b2 & a3 = b3 ) then A2: <*a1,a2,a3*> = <*b1,b2,b3*> by XTUPLE_0:1; ( <*a1,a2,a3*> . 1 = a1 & <*a1,a2,a3*> . 2 = a2 ) by FINSEQ_1:45; hence ( a1 = b1 & a2 = b2 & a3 = b3 ) by A2, A1, FINSEQ_1:45; ::_thesis: verum end; theorem Th14: :: CATALG_1:14 for A being non empty set for S being CatSignature of A for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b) proof let A be non empty set ; ::_thesis: for S being CatSignature of A for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b) let S be CatSignature of A; ::_thesis: for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b) let s be SortSymbol of S; ::_thesis: ex a, b being Element of A st s = homsym (a,b) A1: the carrier of S = [:{0},(2 -tuples_on A):] by Def5; then s `2 in 2 -tuples_on A by MCART_1:10; then s `2 in { z where z is Element of A * : len z = 2 } by FINSEQ_2:def_4; then consider z being Element of A * such that A2: s `2 = z and A3: len z = 2 ; A4: ( z . 1 in {(z . 1),(z . 2)} & z . 2 in {(z . 1),(z . 2)} ) by TARSKI:def_2; A5: z = <*(z . 1),(z . 2)*> by A3, FINSEQ_1:44; then rng z = {(z . 1),(z . 2)} by FINSEQ_2:127; then reconsider a = z . 1, b = z . 2 as Element of A by A4; take a ; ::_thesis: ex b being Element of A st s = homsym (a,b) take b ; ::_thesis: s = homsym (a,b) ( s = [(s `1),(s `2)] & s `1 in {0} ) by A1, MCART_1:10, MCART_1:21; hence s = homsym (a,b) by A2, A5, TARSKI:def_1; ::_thesis: verum end; theorem Th15: :: CATALG_1:15 for A being non empty set for o being OperSymbol of (CatSign A) holds ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) ) proof let A be non empty set ; ::_thesis: for o being OperSymbol of (CatSign A) holds ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) ) let o be OperSymbol of (CatSign A); ::_thesis: ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) ) the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; then ( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def_3; then ( ( o `1 in {1} & o `2 in 1 -tuples_on A ) or ( o `1 in {2} & o `2 in 3 -tuples_on A ) ) by MCART_1:10; hence ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) ) by CARD_1:def_7, TARSKI:def_1; ::_thesis: verum end; theorem Th16: :: CATALG_1:16 for A being non empty set for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds ex a being Element of A st o = idsym a proof let A be non empty set ; ::_thesis: for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds ex a being Element of A st o = idsym a let o be OperSymbol of (CatSign A); ::_thesis: ( ( o `1 = 1 or len (o `2) = 1 ) implies ex a being Element of A st o = idsym a ) assume A1: ( o `1 = 1 or len (o `2) = 1 ) ; ::_thesis: ex a being Element of A st o = idsym a the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; then ( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def_3; then A2: ( ( o `1 in {1} & o `2 in 1 -tuples_on A & o = [(o `1),(o `2)] ) or ( o `1 in {2} & o `2 in 3 -tuples_on A ) ) by MCART_1:10, MCART_1:21; then consider a being set such that A3: a in A and A4: o `2 = <*a*> by A1, CARD_1:def_7, FINSEQ_2:135, TARSKI:def_1; reconsider a = a as Element of A by A3; take a ; ::_thesis: o = idsym a thus o = idsym a by A1, A2, A4, CARD_1:def_7, TARSKI:def_1; ::_thesis: verum end; theorem Th17: :: CATALG_1:17 for A being non empty set for o being OperSymbol of (CatSign A) st ( o `1 = 2 or len (o `2) = 3 ) holds ex a, b, c being Element of A st o = compsym (a,b,c) proof let A be non empty set ; ::_thesis: for o being OperSymbol of (CatSign A) st ( o `1 = 2 or len (o `2) = 3 ) holds ex a, b, c being Element of A st o = compsym (a,b,c) let o be OperSymbol of (CatSign A); ::_thesis: ( ( o `1 = 2 or len (o `2) = 3 ) implies ex a, b, c being Element of A st o = compsym (a,b,c) ) assume A1: ( o `1 = 2 or len (o `2) = 3 ) ; ::_thesis: ex a, b, c being Element of A st o = compsym (a,b,c) the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3; then ( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def_3; then A2: ( ( o `1 in {1} & o `2 in 1 -tuples_on A ) or ( o `1 in {2} & o `2 in 3 -tuples_on A & o = [(o `1),(o `2)] ) ) by MCART_1:10, MCART_1:21; then consider a, b, c being set such that A3: ( a in A & b in A & c in A ) and A4: o `2 = <*a,b,c*> by A1, CARD_1:def_7, FINSEQ_2:139, TARSKI:def_1; reconsider a = a, b = b, c = c as Element of A by A3; take a ; ::_thesis: ex b, c being Element of A st o = compsym (a,b,c) take b ; ::_thesis: ex c being Element of A st o = compsym (a,b,c) take c ; ::_thesis: o = compsym (a,b,c) thus o = compsym (a,b,c) by A1, A2, A4, CARD_1:def_7, TARSKI:def_1; ::_thesis: verum end; theorem :: CATALG_1:18 for A being non empty set for a being Element of A holds ( the_arity_of (idsym a) = {} & the_result_sort_of (idsym a) = homsym (a,a) ) by Def3; theorem :: CATALG_1:19 for A being non empty set for a, b, c being Element of A holds ( the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> & the_result_sort_of (compsym (a,b,c)) = homsym (a,c) ) by Def3; begin definition let C1, C2 be Category; let F be Functor of C1,C2; func Upsilon F -> Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) means :Def11: :: CATALG_1:def 11 for s being SortSymbol of (CatSign the carrier of C1) holds it . s = [0,((Obj F) * (s `2))]; uniqueness for b1, b2 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st ( for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds b2 . s = [0,((Obj F) * (s `2))] ) holds b1 = b2 proof let U1, U2 be Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2); ::_thesis: ( ( for s being SortSymbol of (CatSign the carrier of C1) holds U1 . s = [0,((Obj F) * (s `2))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds U2 . s = [0,((Obj F) * (s `2))] ) implies U1 = U2 ) assume that A1: for s being SortSymbol of (CatSign the carrier of C1) holds U1 . s = [0,((Obj F) * (s `2))] and A2: for s being SortSymbol of (CatSign the carrier of C1) holds U2 . s = [0,((Obj F) * (s `2))] ; ::_thesis: U1 = U2 now__::_thesis:_for_s_being_SortSymbol_of_(CatSign_the_carrier_of_C1)_holds_U1_._s_=_U2_._s let s be SortSymbol of (CatSign the carrier of C1); ::_thesis: U1 . s = U2 . s thus U1 . s = [0,((Obj F) * (s `2))] by A1 .= U2 . s by A2 ; ::_thesis: verum end; hence U1 = U2 by FUNCT_2:63; ::_thesis: verum end; existence ex b1 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))] proof deffunc H1( SortSymbol of (CatSign the carrier of C1)) -> set = [0,((Obj F) * (\$1 `2))]; consider Up being Function such that A3: dom Up = the carrier of (CatSign the carrier of C1) and A4: for s being SortSymbol of (CatSign the carrier of C1) holds Up . s = H1(s) from FUNCT_1:sch_4(); rng Up c= the carrier of (CatSign the carrier of C2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng Up or x in the carrier of (CatSign the carrier of C2) ) assume x in rng Up ; ::_thesis: x in the carrier of (CatSign the carrier of C2) then consider a being set such that A5: a in dom Up and A6: x = Up . a by FUNCT_1:def_3; reconsider a = a as SortSymbol of (CatSign the carrier of C1) by A3, A5; the carrier of (CatSign the carrier of C1) = [:{0},(2 -tuples_on the carrier of C1):] by Def3; then a `2 in 2 -tuples_on the carrier of C1 by MCART_1:12; then consider a1, a2 being set such that A7: ( a1 in the carrier of C1 & a2 in the carrier of C1 ) and A8: a `2 = <*a1,a2*> by FINSEQ_2:137; reconsider a1 = a1, a2 = a2 as Object of C1 by A7; ( rng <*a1,a2*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def_1; then A9: dom ((Obj F) * <*a1,a2*>) = dom <*a1,a2*> by RELAT_1:27 .= Seg 2 by FINSEQ_1:89 ; then reconsider p = (Obj F) * <*a1,a2*> as FinSequence by FINSEQ_1:def_2; ( <*a1,a2*> . 1 = a1 & 1 in {1,2} ) by FINSEQ_1:44, TARSKI:def_2; then A10: p . 1 = (Obj F) . a1 by A9, FINSEQ_1:2, FUNCT_1:12; A11: the carrier of (CatSign the carrier of C2) = [:{0},(2 -tuples_on the carrier of C2):] by Def3; ( <*a1,a2*> . 2 = a2 & 2 in {1,2} ) by FINSEQ_1:44, TARSKI:def_2; then A12: p . 2 = (Obj F) . a2 by A9, FINSEQ_1:2, FUNCT_1:12; len p = 2 by A9, FINSEQ_1:def_3; then p = <*((Obj F) . a1),((Obj F) . a2)*> by A10, A12, FINSEQ_1:44; then p in 2 -tuples_on the carrier of C2 by FINSEQ_2:101; then [0,p] in the carrier of (CatSign the carrier of C2) by A11, ZFMISC_1:105; hence x in the carrier of (CatSign the carrier of C2) by A4, A6, A8; ::_thesis: verum end; then Up is Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) by A3, FUNCT_2:def_1, RELSET_1:4; hence ex b1 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))] by A4; ::_thesis: verum end; func Psi F -> Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) means :Def12: :: CATALG_1:def 12 for o being OperSymbol of (CatSign the carrier of C1) holds it . o = [(o `1),((Obj F) * (o `2))]; uniqueness for b1, b2 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st ( for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds b2 . o = [(o `1),((Obj F) * (o `2))] ) holds b1 = b2 proof let U1, U2 be Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2); ::_thesis: ( ( for o being OperSymbol of (CatSign the carrier of C1) holds U1 . o = [(o `1),((Obj F) * (o `2))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds U2 . o = [(o `1),((Obj F) * (o `2))] ) implies U1 = U2 ) assume that A13: for s being OperSymbol of (CatSign the carrier of C1) holds U1 . s = [(s `1),((Obj F) * (s `2))] and A14: for s being OperSymbol of (CatSign the carrier of C1) holds U2 . s = [(s `1),((Obj F) * (s `2))] ; ::_thesis: U1 = U2 now__::_thesis:_for_s_being_OperSymbol_of_(CatSign_the_carrier_of_C1)_holds_U1_._s_=_U2_._s let s be OperSymbol of (CatSign the carrier of C1); ::_thesis: U1 . s = U2 . s thus U1 . s = [(s `1),((Obj F) * (s `2))] by A13 .= U2 . s by A14 ; ::_thesis: verum end; hence U1 = U2 by FUNCT_2:63; ::_thesis: verum end; existence ex b1 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))] proof deffunc H1( OperSymbol of (CatSign the carrier of C1)) -> set = [(\$1 `1),((Obj F) * (\$1 `2))]; consider Up being Function such that A15: dom Up = the carrier' of (CatSign the carrier of C1) and A16: for s being OperSymbol of (CatSign the carrier of C1) holds Up . s = H1(s) from FUNCT_1:sch_4(); rng Up c= the carrier' of (CatSign the carrier of C2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng Up or x in the carrier' of (CatSign the carrier of C2) ) assume x in rng Up ; ::_thesis: x in the carrier' of (CatSign the carrier of C2) then consider a being set such that A17: a in dom Up and A18: x = Up . a by FUNCT_1:def_3; A19: the carrier' of (CatSign the carrier of C1) = [:{1},(1 -tuples_on the carrier of C1):] \/ [:{2},(3 -tuples_on the carrier of C1):] by Def3; reconsider a = a as OperSymbol of (CatSign the carrier of C1) by A15, A17; percases ( a in [:{1},(1 -tuples_on the carrier of C1):] or a in [:{2},(3 -tuples_on the carrier of C1):] ) by A19, XBOOLE_0:def_3; supposeA20: a in [:{1},(1 -tuples_on the carrier of C1):] ; ::_thesis: x in the carrier' of (CatSign the carrier of C2) then a `2 in 1 -tuples_on the carrier of C1 by MCART_1:12; then consider a1 being set such that A21: a1 in the carrier of C1 and A22: a `2 = <*a1*> by FINSEQ_2:135; reconsider a1 = a1 as Object of C1 by A21; ( rng <*a1*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def_1; then A23: dom ((Obj F) * <*a1*>) = dom <*a1*> by RELAT_1:27 .= Seg 1 by FINSEQ_1:38 ; then reconsider p = (Obj F) * <*a1*> as FinSequence by FINSEQ_1:def_2; A24: len p = 1 by A23, FINSEQ_1:def_3; ( <*a1*> . 1 = a1 & 1 in {1} ) by FINSEQ_1:40, TARSKI:def_1; then p . 1 = (Obj F) . a1 by A23, FINSEQ_1:2, FUNCT_1:12; then p = <*((Obj F) . a1)*> by A24, FINSEQ_1:40; then p is Element of 1 -tuples_on the carrier of C2 by FINSEQ_2:98; then A25: [1,p] in [:{1},(1 -tuples_on the carrier of C2):] by ZFMISC_1:105; A26: a `1 = 1 by A20, MCART_1:12; the carrier' of (CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] by Def3; then [1,p] in the carrier' of (CatSign the carrier of C2) by A25, XBOOLE_0:def_3; hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A26, A22; ::_thesis: verum end; supposeA27: a in [:{2},(3 -tuples_on the carrier of C1):] ; ::_thesis: x in the carrier' of (CatSign the carrier of C2) then a `2 in 3 -tuples_on the carrier of C1 by MCART_1:12; then consider a1, a2, a3 being set such that A28: ( a1 in the carrier of C1 & a2 in the carrier of C1 & a3 in the carrier of C1 ) and A29: a `2 = <*a1,a2,a3*> by FINSEQ_2:139; reconsider a1 = a1, a2 = a2, a3 = a3 as Object of C1 by A28; ( rng <*a1,a2,a3*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def_1; then A30: dom ((Obj F) * <*a1,a2,a3*>) = dom <*a1,a2,a3*> by RELAT_1:27 .= Seg 3 by FINSEQ_1:89 ; then reconsider p = (Obj F) * <*a1,a2,a3*> as FinSequence by FINSEQ_1:def_2; ( <*a1,a2,a3*> . 1 = a1 & 1 in {1,2,3} ) by ENUMSET1:def_1, FINSEQ_1:45; then A31: p . 1 = (Obj F) . a1 by A30, FINSEQ_3:1, FUNCT_1:12; ( <*a1,a2,a3*> . 3 = a3 & 3 in {1,2,3} ) by ENUMSET1:def_1, FINSEQ_1:45; then A32: p . 3 = (Obj F) . a3 by A30, FINSEQ_3:1, FUNCT_1:12; ( <*a1,a2,a3*> . 2 = a2 & 2 in {1,2,3} ) by ENUMSET1:def_1, FINSEQ_1:45; then A33: p . 2 = (Obj F) . a2 by A30, FINSEQ_3:1, FUNCT_1:12; len p = 3 by A30, FINSEQ_1:def_3; then p = <*((Obj F) . a1),((Obj F) . a2),((Obj F) . a3)*> by A31, A33, A32, FINSEQ_1:45; then p is Element of 3 -tuples_on the carrier of C2 by FINSEQ_2:104; then A34: [2,p] in [:{2},(3 -tuples_on the carrier of C2):] by ZFMISC_1:105; A35: a `1 = 2 by A27, MCART_1:12; the carrier' of (CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] by Def3; then [2,p] in the carrier' of (CatSign the carrier of C2) by A34, XBOOLE_0:def_3; hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A35, A29; ::_thesis: verum end; end; end; then Up is Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) by A15, FUNCT_2:def_1, RELSET_1:4; hence ex b1 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))] by A16; ::_thesis: verum end; end; :: deftheorem Def11 defines Upsilon CATALG_1:def_11_:_ for C1, C2 being Category for F being Functor of C1,C2 for b4 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) holds ( b4 = Upsilon F iff for s being SortSymbol of (CatSign the carrier of C1) holds b4 . s = [0,((Obj F) * (s `2))] ); :: deftheorem Def12 defines Psi CATALG_1:def_12_:_ for C1, C2 being Category for F being Functor of C1,C2 for b4 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) holds ( b4 = Psi F iff for o being OperSymbol of (CatSign the carrier of C1) holds b4 . o = [(o `1),((Obj F) * (o `2))] ); Lm2: now__::_thesis:_for_x_being_set_ for_f_being_Function_st_x_in_dom_f_holds_ f_*_<*x*>_=_<*(f_._x)*> let x be set ; ::_thesis: for f being Function st x in dom f holds f * <*x*> = <*(f . x)*> let f be Function; ::_thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> ) assume x in dom f ; ::_thesis: f * <*x*> = <*(f . x)*> then ( rng <*x*> = {x} & {x} c= dom f ) by FINSEQ_1:39, ZFMISC_1:31; then A1: dom (f * <*x*>) = dom <*x*> by RELAT_1:27 .= Seg 1 by FINSEQ_1:38 ; then reconsider p = f * <*x*> as FinSequence by FINSEQ_1:def_2; A2: len p = 1 by A1, FINSEQ_1:def_3; ( 1 in {1} & <*x*> . 1 = x ) by FINSEQ_1:40, TARSKI:def_1; then p . 1 = f . x by A1, FINSEQ_1:2, FUNCT_1:12; hence f * <*x*> = <*(f . x)*> by A2, FINSEQ_1:40; ::_thesis: verum end; theorem Th20: :: CATALG_1:20 for C1, C2 being Category for F being Functor of C1,C2 for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b)) proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b)) let F be Functor of C1,C2; ::_thesis: for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b)) let a, b be Object of C1; ::_thesis: (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b)) A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def_1; thus (Upsilon F) . (homsym (a,b)) = [0,((Obj F) * ((homsym (a,b)) `2))] by Def11 .= [0,((Obj F) * <*a,b*>)] by MCART_1:7 .= [0,<*((Obj F) . a),((Obj F) . b)*>] by A1, FINSEQ_2:125 .= [0,<*(F . a),((Obj F) . b)*>] .= homsym ((F . a),(F . b)) ; ::_thesis: verum end; theorem Th21: :: CATALG_1:21 for C1, C2 being Category for F being Functor of C1,C2 for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a) proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a) let F be Functor of C1,C2; ::_thesis: for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a) let a be Object of C1; ::_thesis: (Psi F) . (idsym a) = idsym (F . a) A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def_1; ( (idsym a) `1 = 1 & (idsym a) `2 = <*a*> ) by MCART_1:7; hence (Psi F) . (idsym a) = [1,((Obj F) * <*a*>)] by Def12 .= [1,<*((Obj F) . a)*>] by A1, Lm2 .= idsym (F . a) ; ::_thesis: verum end; theorem Th22: :: CATALG_1:22 for C1, C2 being Category for F being Functor of C1,C2 for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c)) proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c)) let F be Functor of C1,C2; ::_thesis: for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c)) let a, b, c be Object of C1; ::_thesis: (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c)) A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def_1; ( (compsym (a,b,c)) `1 = 2 & (compsym (a,b,c)) `2 = <*a,b,c*> ) by MCART_1:7; hence (Psi F) . (compsym (a,b,c)) = [2,((Obj F) * <*a,b,c*>)] by Def12 .= [2,<*((Obj F) . a),((Obj F) . b),((Obj F) . c)*>] by A1, FINSEQ_2:126 .= [2,<*(F . a),((Obj F) . b),((Obj F) . c)*>] .= [2,<*(F . a),(F . b),((Obj F) . c)*>] .= compsym ((F . a),(F . b),(F . c)) ; ::_thesis: verum end; theorem Th23: :: CATALG_1:23 for C1, C2 being Category for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 let F be Functor of C1,C2; ::_thesis: Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 set f = Upsilon F; set g = Psi F; set S1 = CatSign the carrier of C1; set S2 = CatSign the carrier of C2; thus ( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & dom (Psi F) = the carrier' of (CatSign the carrier of C1) ) by FUNCT_2:def_1; :: according to PUA2MSS1:def_12 ::_thesis: ( proj2 (Upsilon F) c= the carrier of (CatSign the carrier of C2) & proj2 (Psi F) c= the carrier' of (CatSign the carrier of C2) & the ResultSort of (CatSign the carrier of C1) * (Upsilon F) = (Psi F) * the ResultSort of (CatSign the carrier of C2) & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of (CatSign the carrier of C1) or not b2 = the Arity of (CatSign the carrier of C1) . b1 or b2 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b1) ) ) ) thus ( rng (Upsilon F) c= the carrier of (CatSign the carrier of C2) & rng (Psi F) c= the carrier' of (CatSign the carrier of C2) ) ; ::_thesis: ( the ResultSort of (CatSign the carrier of C1) * (Upsilon F) = (Psi F) * the ResultSort of (CatSign the carrier of C2) & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of (CatSign the carrier of C1) or not b2 = the Arity of (CatSign the carrier of C1) . b1 or b2 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b1) ) ) ) now__::_thesis:_for_o_being_OperSymbol_of_(CatSign_the_carrier_of_C1)_holds_((Upsilon_F)_*_the_ResultSort_of_(CatSign_the_carrier_of_C1))_._o_=_(_the_ResultSort_of_(CatSign_the_carrier_of_C2)_*_(Psi_F))_._o let o be OperSymbol of (CatSign the carrier of C1); ::_thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b1 = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b1 percases ( o `1 = 1 or o `1 = 2 ) by Th15; suppose o `1 = 1 ; ::_thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b1 = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b1 then consider a being Object of C1 such that A1: o = idsym a by Th16; thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:15 .= (Upsilon F) . (homsym (a,a)) by A1, Def3 .= homsym ((F . a),(F . a)) by Th20 .= the_result_sort_of (idsym (F . a)) by Def3 .= the ResultSort of (CatSign the carrier of C2) . ((Psi F) . (idsym a)) by Th21 .= ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A1, FUNCT_2:15 ; ::_thesis: verum end; suppose o `1 = 2 ; ::_thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b1 = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b1 then consider a, b, c being Object of C1 such that A2: o = compsym (a,b,c) by Th17; thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:15 .= (Upsilon F) . (homsym (a,c)) by A2, Def3 .= homsym ((F . a),(F . c)) by Th20 .= the_result_sort_of (compsym ((F . a),(F . b),(F . c))) by Def3 .= the ResultSort of (CatSign the carrier of C2) . ((Psi F) . (compsym (a,b,c))) by Th22 .= ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A2, FUNCT_2:15 ; ::_thesis: verum end; end; end; hence (Upsilon F) * the ResultSort of (CatSign the carrier of C1) = the ResultSort of (CatSign the carrier of C2) * (Psi F) by FUNCT_2:63; ::_thesis: for b1 being set for b2 being set holds ( not b1 in the carrier' of (CatSign the carrier of C1) or not b2 = the Arity of (CatSign the carrier of C1) . b1 or b2 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b1) ) let o be set ; ::_thesis: for b1 being set holds ( not o in the carrier' of (CatSign the carrier of C1) or not b1 = the Arity of (CatSign the carrier of C1) . o or b1 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) ) let p be Function; ::_thesis: ( not o in the carrier' of (CatSign the carrier of C1) or not p = the Arity of (CatSign the carrier of C1) . o or p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) ) assume o in the carrier' of (CatSign the carrier of C1) ; ::_thesis: ( not p = the Arity of (CatSign the carrier of C1) . o or p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) ) then reconsider o9 = o as OperSymbol of (CatSign the carrier of C1) ; assume A3: p = the Arity of (CatSign the carrier of C1) . o ; ::_thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) percases ( o9 `1 = 1 or o9 `1 = 2 ) by Th15; suppose o9 `1 = 1 ; ::_thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) then consider a being Object of C1 such that A4: o = idsym a by Th16; A5: (Upsilon F) * {} = {} ; p = {} by A3, A4, Def3; hence (Upsilon F) * p = the_arity_of (idsym (F . a)) by A5, Def3 .= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A4, Th21 ; ::_thesis: verum end; suppose o9 `1 = 2 ; ::_thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) then consider a, b, c being Object of C1 such that A6: o = compsym (a,b,c) by Th17; ( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & p = <*(homsym (b,c)),(homsym (a,b))*> ) by A3, A6, Def3, FUNCT_2:def_1; hence (Upsilon F) * p = <*((Upsilon F) . (homsym (b,c))),((Upsilon F) . (homsym (a,b)))*> by FINSEQ_2:125 .= <*(homsym ((F . b),(F . c))),((Upsilon F) . (homsym (a,b)))*> by Th20 .= <*(homsym ((F . b),(F . c))),(homsym ((F . a),(F . b)))*> by Th20 .= the_arity_of (compsym ((F . a),(F . b),(F . c))) by Def3 .= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A6, Th22 ; ::_thesis: verum end; end; end; begin theorem Th24: :: CATALG_1:24 for C being non empty set for A being MSAlgebra over CatSign C for a being Element of C holds Args ((idsym a),A) = {{}} proof let C be non empty set ; ::_thesis: for A being MSAlgebra over CatSign C for a being Element of C holds Args ((idsym a),A) = {{}} let A be MSAlgebra over CatSign C; ::_thesis: for a being Element of C holds Args ((idsym a),A) = {{}} let a be Element of C; ::_thesis: Args ((idsym a),A) = {{}} thus Args ((idsym a),A) = product ( the Sorts of A * (the_arity_of (idsym a))) by PRALG_2:3 .= product ( the Sorts of A * {}) by Def3 .= {{}} by CARD_3:10 ; ::_thesis: verum end; Lm3: for C being Category for A being MSAlgebra over CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) holds for a, b, c being Object of C holds ( Args ((compsym (a,b,c)),A) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),A) = Hom (a,c) ) proof let C be Category; ::_thesis: for A being MSAlgebra over CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) holds for a, b, c being Object of C holds ( Args ((compsym (a,b,c)),A) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),A) = Hom (a,c) ) let A be MSAlgebra over CatSign the carrier of C; ::_thesis: ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) implies for a, b, c being Object of C holds ( Args ((compsym (a,b,c)),A) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),A) = Hom (a,c) ) ) assume A1: for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ; ::_thesis: for a, b, c being Object of C holds ( Args ((compsym (a,b,c)),A) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),A) = Hom (a,c) ) let a, b, c be Object of C; ::_thesis: ( Args ((compsym (a,b,c)),A) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),A) = Hom (a,c) ) A2: the carrier of (CatSign the carrier of C) = dom the Sorts of A by PARTFUN1:def_2; thus Args ((compsym (a,b,c)),A) = product ( the Sorts of A * (the_arity_of (compsym (a,b,c)))) by PRALG_2:3 .= product ( the Sorts of A * <*(homsym (b,c)),(homsym (a,b))*>) by Def3 .= product <*( the Sorts of A . (homsym (b,c))),( the Sorts of A . (homsym (a,b)))*> by A2, FINSEQ_2:125 .= product <*(Hom (b,c)),( the Sorts of A . (homsym (a,b)))*> by A1 .= product <*(Hom (b,c)),(Hom (a,b))*> by A1 ; ::_thesis: Result ((compsym (a,b,c)),A) = Hom (a,c) thus Result ((compsym (a,b,c)),A) = the Sorts of A . (the_result_sort_of (compsym (a,b,c))) by PRALG_2:3 .= the Sorts of A . (homsym (a,c)) by Def3 .= Hom (a,c) by A1 ; ::_thesis: verum end; scheme :: CATALG_1:sch 1 CatAlgEx{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set , set , set , set ) -> set , F5( set ) -> set } : ex A being strict MSAlgebra over CatSign F1() st ( ( for a, b being Element of F1() holds the Sorts of A . (homsym (a,b)) = F3(a,b) ) & ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) & ( for a, b, c being Element of F1() for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) ) provided A1: for a, b being Element of F1() holds F3(a,b) c= F2() and A2: for a being Element of F1() holds F5(a) in F3(a,a) and A3: for a, b, c being Element of F1() for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds F4(a,b,c,g,f) in F3(a,c) proof defpred S1[ set , set ] means ( ( \$1 `1 = 1 & ex a being Element of F1() st ( \$1 = idsym a & ex F being Function of {{}},F3(a,a) st ( F = \$2 & F . {} = F5(a) ) ) ) or ( \$1 `1 = 2 & ex a, b, c being Element of F1() st ( \$1 = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = \$2 & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) ) ) ); set CS = CatSign F1(); A4: for o being set st o in the carrier' of (CatSign F1()) holds ex u being set st S1[o,u] proof let o be set ; ::_thesis: ( o in the carrier' of (CatSign F1()) implies ex u being set st S1[o,u] ) assume A5: o in the carrier' of (CatSign F1()) ; ::_thesis: ex u being set st S1[o,u] A6: now__::_thesis:_(_o_`1_=_1_implies_ex_u_being_set_ex_a_being_Element_of_F1()_st_ (_o_=_idsym_a_&_ex_F_being_Function_of_{{}},F3(a,a)_st_ (_F_=_u_&_F_._{}_=_F5(a)_)_)_) assume o `1 = 1 ; ::_thesis: ex u being set ex a being Element of F1() st ( o = idsym a & ex F being Function of {{}},F3(a,a) st ( F = u & F . {} = F5(a) ) ) then consider a being Element of F1() such that A7: o = idsym a by A5, Th16; set F = {} :-> F5(a); reconsider u = {} :-> F5(a) as set ; take u = u; ::_thesis: ex a being Element of F1() st ( o = idsym a & ex F being Function of {{}},F3(a,a) st ( F = u & F . {} = F5(a) ) ) take a = a; ::_thesis: ( o = idsym a & ex F being Function of {{}},F3(a,a) st ( F = u & F . {} = F5(a) ) ) thus o = idsym a by A7; ::_thesis: ex F being Function of {{}},F3(a,a) st ( F = u & F . {} = F5(a) ) F5(a) in F3(a,a) by A2; then {F5(a)} c= F3(a,a) by ZFMISC_1:31; then ( dom ({} :-> F5(a)) = {{}} & rng ({} :-> F5(a)) c= F3(a,a) ) by FUNCOP_1:13, XBOOLE_1:1; then reconsider F = {} :-> F5(a) as Function of {{}},F3(a,a) by FUNCT_2:2; take F = F; ::_thesis: ( F = u & F . {} = F5(a) ) {} in {{}} by TARSKI:def_1; hence ( F = u & F . {} = F5(a) ) by FUNCOP_1:7; ::_thesis: verum end; A8: now__::_thesis:_(_o_`1_=_2_implies_ex_u_being_set_ex_a,_b,_c_being_Element_of_F1()_st_ (_o_=_compsym_(a,b,c)_&_ex_F_being_Function_of_(product_<*F3(b,c),F3(a,b)*>),F3(a,c)_st_ (_F_=_u_&_(_for_f,_g_being_set_st_f_in_F3(a,b)_&_g_in_F3(b,c)_holds_ F_._<*g,f*>_=_F4(a,b,c,g,f)_)_)_)_) assume o `1 = 2 ; ::_thesis: ex u being set ex a, b, c being Element of F1() st ( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) ) then consider a, b, c being Element of F1() such that A9: o = compsym (a,b,c) by A5, Th17; defpred S2[ set , set ] means ex f, g being set st ( f in F3(a,b) & g in F3(b,c) & \$1 = <*g,f*> & \$2 = F4(a,b,c,g,f) ); A10: now__::_thesis:_for_x_being_set_st_x_in_product_<*F3(b,c),F3(a,b)*>_holds_ ex_u_being_set_st_ (_u_in_F3(a,c)_&_S2[x,u]_) let x be set ; ::_thesis: ( x in product <*F3(b,c),F3(a,b)*> implies ex u being set st ( u in F3(a,c) & S2[x,u] ) ) assume x in product <*F3(b,c),F3(a,b)*> ; ::_thesis: ex u being set st ( u in F3(a,c) & S2[x,u] ) then consider g, f being set such that A11: ( g in F3(b,c) & f in F3(a,b) ) and A12: x = <*g,f*> by FINSEQ_3:124; take u = F4(a,b,c,g,f); ::_thesis: ( u in F3(a,c) & S2[x,u] ) ( F3(a,b) c= F2() & F3(b,c) c= F2() ) by A1; hence u in F3(a,c) by A3, A11; ::_thesis: S2[x,u] thus S2[x,u] by A11, A12; ::_thesis: verum end; consider F being Function such that A13: ( dom F = product <*F3(b,c),F3(a,b)*> & rng F c= F3(a,c) ) and A14: for x being set st x in product <*F3(b,c),F3(a,b)*> holds S2[x,F . x] from FUNCT_1:sch_5(A10); reconsider u = F as set ; take u = u; ::_thesis: ex a, b, c being Element of F1() st ( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) ) take a = a; ::_thesis: ex b, c being Element of F1() st ( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) ) take b = b; ::_thesis: ex c being Element of F1() st ( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) ) take c = c; ::_thesis: ( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) ) thus o = compsym (a,b,c) by A9; ::_thesis: ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) reconsider F = F as Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) by A13, FUNCT_2:2; take F = F; ::_thesis: ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) thus F = u ; ::_thesis: for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) let f, g be set ; ::_thesis: ( f in F3(a,b) & g in F3(b,c) implies F . <*g,f*> = F4(a,b,c,g,f) ) assume ( f in F3(a,b) & g in F3(b,c) ) ; ::_thesis: F . <*g,f*> = F4(a,b,c,g,f) then <*g,f*> in product <*F3(b,c),F3(a,b)*> by FINSEQ_3:124; then consider f9, g9 being set such that f9 in F3(a,b) and g9 in F3(b,c) and A15: <*g,f*> = <*g9,f9*> and A16: F . <*g,f*> = F4(a,b,c,g9,f9) by A14; A17: ( <*g,f*> . 1 = g & <*g,f*> . 2 = f ) by FINSEQ_1:44; <*g,f*> . 1 = g9 by A15, FINSEQ_1:44; hence F . <*g,f*> = F4(a,b,c,g,f) by A15, A16, A17, FINSEQ_1:44; ::_thesis: verum end; ( o `1 = 1 or o `1 = 2 ) by A5, Th15; hence ex u being set st S1[o,u] by A6, A8; ::_thesis: verum end; consider O being Function such that A18: dom O = the carrier' of (CatSign F1()) and A19: for o being set st o in the carrier' of (CatSign F1()) holds S1[o,O . o] from CLASSES1:sch_1(A4); reconsider O = O as ManySortedSet of the carrier' of (CatSign F1()) by A18, PARTFUN1:def_2, RELAT_1:def_18; defpred S2[ set , set ] means ex a, b being Element of F1() st ( \$1 = homsym (a,b) & \$2 = F3(a,b) ); A20: now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_(CatSign_F1())_holds_ ex_u_being_set_st_S2[s,u] let s be set ; ::_thesis: ( s in the carrier of (CatSign F1()) implies ex u being set st S2[s,u] ) assume s in the carrier of (CatSign F1()) ; ::_thesis: ex u being set st S2[s,u] then consider a, b being Element of F1() such that A21: s = homsym (a,b) by Th14; take u = F3(a,b); ::_thesis: S2[s,u] thus S2[s,u] by A21; ::_thesis: verum end; consider S being Function such that A22: dom S = the carrier of (CatSign F1()) and A23: for s being set st s in the carrier of (CatSign F1()) holds S2[s,S . s] from CLASSES1:sch_1(A20); reconsider S = S as ManySortedSet of the carrier of (CatSign F1()) by A22, PARTFUN1:def_2, RELAT_1:def_18; O is ManySortedFunction of (S #) * the Arity of (CatSign F1()),S * the ResultSort of (CatSign F1()) proof let o be set ; :: according to PBOOLE:def_15 ::_thesis: ( not o in the carrier' of (CatSign F1()) or O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] ) assume o in the carrier' of (CatSign F1()) ; ::_thesis: O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] then reconsider o = o as OperSymbol of (CatSign F1()) ; A24: ((S #) * the Arity of (CatSign F1())) . o = (S #) . (the_arity_of o) by FUNCT_2:15 .= product (S * (the_arity_of o)) by FINSEQ_2:def_5 ; A25: (S * the ResultSort of (CatSign F1())) . o = S . (the_result_sort_of o) by FUNCT_2:15; percases ( ( o `1 = 1 & 1 <> 2 ) or ( o `1 = 2 & 1 <> 2 ) ) by Th15; suppose ( o `1 = 1 & 1 <> 2 ) ; ::_thesis: O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] then consider a being Element of F1() such that A26: ( o = idsym a & ex F being Function of {{}},F3(a,a) st ( F = O . o & F . {} = F5(a) ) ) by A19; A27: ( the_arity_of (idsym a) = {} & {} = S * {} ) by Def3; A28: the_result_sort_of (idsym a) = homsym (a,a) by Def3; consider c, b being Element of F1() such that A29: homsym (a,a) = homsym (c,b) and A30: S . (homsym (a,a)) = F3(c,b) by A23; ( a = b & a = c ) by A29, Th12; hence O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] by A24, A25, A26, A30, A27, A28, CARD_3:10; ::_thesis: verum end; suppose ( o `1 = 2 & 1 <> 2 ) ; ::_thesis: O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] then consider a, b, c being Element of F1() such that A31: o = compsym (a,b,c) and A32: ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st ( F = O . o & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds F . <*g,f*> = F4(a,b,c,g,f) ) ) by A19; A33: the_result_sort_of (compsym (a,b,c)) = homsym (a,c) by Def3; consider ax, cx being Element of F1() such that A34: homsym (a,c) = homsym (ax,cx) and A35: S . (homsym (a,c)) = F3(ax,cx) by A23; ( ax = a & cx = c ) by A34, Th12; then A36: (S * the ResultSort of (CatSign F1())) . o = F3(a,c) by A31, A35, A33, FUNCT_2:15; A37: the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> by Def3; consider a9, b9 being Element of F1() such that A38: homsym (a,b) = homsym (a9,b9) and A39: S . (homsym (a,b)) = F3(a9,b9) by A23; consider b99, c9 being Element of F1() such that A40: homsym (b,c) = homsym (b99,c9) and A41: S . (homsym (b,c)) = F3(b99,c9) by A23; A42: ( b99 = b & c9 = c ) by A40, Th12; ( a9 = a & b9 = b ) by A38, Th12; then ((S #) * the Arity of (CatSign F1())) . o = product <*F3(b,c),F3(a,b)*> by A22, A24, A31, A39, A41, A42, A37, FINSEQ_2:125; hence O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] by A32, A36; ::_thesis: verum end; end; end; then reconsider O = O as ManySortedFunction of (S #) * the Arity of (CatSign F1()),S * the ResultSort of (CatSign F1()) ; take A = MSAlgebra(# S,O #); ::_thesis: ( ( for a, b being Element of F1() holds the Sorts of A . (homsym (a,b)) = F3(a,b) ) & ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) & ( for a, b, c being Element of F1() for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) ) hereby ::_thesis: ( ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) & ( for a, b, c being Element of F1() for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) ) let a, b be Element of F1(); ::_thesis: the Sorts of A . (homsym (a,b)) = F3(a,b) consider a9, b9 being Element of F1() such that A43: homsym (a,b) = homsym (a9,b9) and A44: S . (homsym (a,b)) = F3(a9,b9) by A23; a = a9 by A43, Th12; hence the Sorts of A . (homsym (a,b)) = F3(a,b) by A43, A44, Th12; ::_thesis: verum end; hereby ::_thesis: for a, b, c being Element of F1() for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) let a be Element of F1(); ::_thesis: (Den ((idsym a),A)) . {} = F5(a) (idsym a) `1 = 1 by MCART_1:7; then ex b being Element of F1() st ( idsym a = idsym b & ex F being Function of {{}},F3(b,b) st ( F = O . (idsym a) & F . {} = F5(b) ) ) by A19; hence (Den ((idsym a),A)) . {} = F5(a) by Th11; ::_thesis: verum end; let a, b, c be Element of F1(); ::_thesis: for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) set o = compsym (a,b,c); (compsym (a,b,c)) `1 = 2 by MCART_1:7; then consider a9, b9, c9 being Element of F1() such that A45: compsym (a,b,c) = compsym (a9,b9,c9) and A46: ex F being Function of (product <*F3(b9,c9),F3(a9,b9)*>),F3(a9,c9) st ( F = O . (compsym (a,b,c)) & ( for f, g being set st f in F3(a9,b9) & g in F3(b9,c9) holds F . <*g,f*> = F4(a9,b9,c9,g,f) ) ) by A19; A47: c = c9 by A45, Th13; let f, g be Element of F2(); ::_thesis: ( f in F3(a,b) & g in F3(b,c) implies (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) assume A48: ( f in F3(a,b) & g in F3(b,c) ) ; ::_thesis: (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ( a = a9 & b = b9 ) by A45, Th13; hence (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) by A46, A47, A48; ::_thesis: verum end; definition let C be Category; func MSAlg C -> strict MSAlgebra over CatSign the carrier of C means :Def13: :: CATALG_1:def 13 ( ( for a, b being Object of C holds the Sorts of it . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),it)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),it)) . <*g,f*> = g (*) f ) ); uniqueness for b1, b2 being strict MSAlgebra over CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of b1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b1)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),b1)) . <*g,f*> = g (*) f ) & ( for a, b being Object of C holds the Sorts of b2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b2)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),b2)) . <*g,f*> = g (*) f ) holds b1 = b2 proof let A1, A2 be strict MSAlgebra over CatSign the carrier of C; ::_thesis: ( ( for a, b being Object of C holds the Sorts of A1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A1)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A1)) . <*g,f*> = g (*) f ) & ( for a, b being Object of C holds the Sorts of A2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A2)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A2)) . <*g,f*> = g (*) f ) implies A1 = A2 ) assume that A1: for a, b being Object of C holds the Sorts of A1 . (homsym (a,b)) = Hom (a,b) and A2: for a being Object of C holds (Den ((idsym a),A1)) . {} = id a and A3: for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A1)) . <*g,f*> = g (*) f and A4: for a, b being Object of C holds the Sorts of A2 . (homsym (a,b)) = Hom (a,b) and A5: for a being Object of C holds (Den ((idsym a),A2)) . {} = id a and A6: for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A2)) . <*g,f*> = g (*) f ; ::_thesis: A1 = A2 A7: now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_(CatSign_the_carrier_of_C)_holds_ the_Charact_of_A1_._i_=_the_Charact_of_A2_._i let i be set ; ::_thesis: ( i in the carrier' of (CatSign the carrier of C) implies the Charact of A1 . b1 = the Charact of A2 . b1 ) assume i in the carrier' of (CatSign the carrier of C) ; ::_thesis: the Charact of A1 . b1 = the Charact of A2 . b1 then reconsider o = i as OperSymbol of (CatSign the carrier of C) ; percases ( o `1 = 1 or o `1 = 2 ) by Th15; suppose o `1 = 1 ; ::_thesis: the Charact of A1 . b1 = the Charact of A2 . b1 then consider a being Object of C such that A8: o = idsym a by Th16; A9: id a in Hom (a,a) by CAT_1:27; A10: the_result_sort_of (idsym a) = homsym (a,a) by Def3; the Sorts of A1 . (homsym (a,a)) = Hom (a,a) by A1; then Result ((idsym a),A1) = Hom (a,a) by A10, PRALG_2:3; then A11: dom (Den ((idsym a),A1)) = Args ((idsym a),A1) by A9, FUNCT_2:def_1; A12: now__::_thesis:_for_x_being_set_st_x_in_{{}}_holds_ (Den_((idsym_a),A1))_._x_=_(Den_((idsym_a),A2))_._x let x be set ; ::_thesis: ( x in {{}} implies (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x ) assume x in {{}} ; ::_thesis: (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x then A13: x = {} by TARSKI:def_1; then (Den ((idsym a),A1)) . x = id a by A2; hence (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x by A5, A13; ::_thesis: verum end; the Sorts of A2 . (homsym (a,a)) = Hom (a,a) by A4; then Result ((idsym a),A2) = Hom (a,a) by A10, PRALG_2:3; then A14: dom (Den ((idsym a),A2)) = Args ((idsym a),A2) by A9, FUNCT_2:def_1; ( Args ((idsym a),A1) = {{}} & Args ((idsym a),A2) = {{}} ) by Th24; hence the Charact of A1 . i = the Charact of A2 . i by A8, A11, A14, A12, FUNCT_1:2; ::_thesis: verum end; suppose o `1 = 2 ; ::_thesis: the Charact of A1 . b1 = the Charact of A2 . b1 then consider a, b, c being Object of C such that A15: o = compsym (a,b,c) by Th17; A16: now__::_thesis:_(_product_<*(Hom_(b,c)),(Hom_(a,b))*>_<>_{}_implies_Hom_(a,c)_<>_{}_) assume product <*(Hom (b,c)),(Hom (a,b))*> <> {} ; ::_thesis: Hom (a,c) <> {} then reconsider X = product <*(Hom (b,c)),(Hom (a,b))*> as non empty set ; set x = the Element of X; consider g, f being set such that A17: g in Hom (b,c) and A18: f in Hom (a,b) and the Element of X = <*g,f*> by FINSEQ_3:124; reconsider g = g, f = f as Morphism of C by A17, A18; A19: ( cod f = b & dom g = b ) by A17, A18, CAT_1:1; cod g = c by A17, CAT_1:1; then A20: cod (g (*) f) = c by A19, CAT_1:17; dom f = a by A18, CAT_1:1; then dom (g (*) f) = a by A19, CAT_1:17; hence Hom (a,c) <> {} by A20, CAT_1:1; ::_thesis: verum end; A21: now__::_thesis:_for_x_being_set_st_x_in_product_<*(Hom_(b,c)),(Hom_(a,b))*>_holds_ (Den_((compsym_(a,b,c)),A1))_._x_=_(Den_((compsym_(a,b,c)),A2))_._x let x be set ; ::_thesis: ( x in product <*(Hom (b,c)),(Hom (a,b))*> implies (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x ) assume x in product <*(Hom (b,c)),(Hom (a,b))*> ; ::_thesis: (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x then consider g, f being set such that A22: g in Hom (b,c) and A23: f in Hom (a,b) and A24: x = <*g,f*> by FINSEQ_3:124; reconsider g = g, f = f as Morphism of C by A22, A23; A25: ( dom g = b & cod g = c ) by A22, CAT_1:1; A26: ( dom f = a & cod f = b ) by A23, CAT_1:1; then (Den ((compsym (a,b,c)),A1)) . x = g (*) f by A3, A24, A25; hence (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x by A6, A24, A26, A25; ::_thesis: verum end; A27: Args ((compsym (a,b,c)),A1) = product <*(Hom (b,c)),(Hom (a,b))*> by A1, Lm3; A28: Args ((compsym (a,b,c)),A2) = product <*(Hom (b,c)),(Hom (a,b))*> by A4, Lm3; Result ((compsym (a,b,c)),A2) = Hom (a,c) by A4, Lm3; then A29: dom (Den ((compsym (a,b,c)),A2)) = Args ((compsym (a,b,c)),A2) by A28, A16, FUNCT_2:def_1; Result ((compsym (a,b,c)),A1) = Hom (a,c) by A1, Lm3; then dom (Den ((compsym (a,b,c)),A1)) = Args ((compsym (a,b,c)),A1) by A27, A16, FUNCT_2:def_1; hence the Charact of A1 . i = the Charact of A2 . i by A15, A27, A28, A29, A21, FUNCT_1:2; ::_thesis: verum end; end; end; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_(CatSign_the_carrier_of_C)_holds_ the_Sorts_of_A1_._i_=_the_Sorts_of_A2_._i let i be set ; ::_thesis: ( i in the carrier of (CatSign the carrier of C) implies the Sorts of A1 . i = the Sorts of A2 . i ) assume i in the carrier of (CatSign the carrier of C) ; ::_thesis: the Sorts of A1 . i = the Sorts of A2 . i then consider a, b being Object of C such that A30: i = homsym (a,b) by Th14; thus the Sorts of A1 . i = Hom (a,b) by A1, A30 .= the Sorts of A2 . i by A4, A30 ; ::_thesis: verum end; then the Sorts of A1 = the Sorts of A2 by PBOOLE:3; hence A1 = A2 by A7, PBOOLE:3; ::_thesis: verum end; correctness existence ex b1 being strict MSAlgebra over CatSign the carrier of C st ( ( for a, b being Object of C holds the Sorts of b1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b1)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),b1)) . <*g,f*> = g (*) f ) ); proof deffunc H1( Object of C) -> Morphism of \$1,\$1 = id \$1; deffunc H2( Object of C, Object of C, Object of C, Morphism of C, Morphism of C) -> Element of the carrier' of C = \$4 (*) \$5; deffunc H3( Object of C, Object of C) -> Element of bool the carrier' of C = Hom (\$1,\$2); A31: for a being Object of C holds H1(a) in H3(a,a) by CAT_1:27; A32: now__::_thesis:_for_a,_b,_c_being_Object_of_C for_f,_g_being_Morphism_of_C_st_f_in_H3(a,b)_&_g_in_H3(b,c)_holds_ H2(a,b,c,g,f)_in_H3(a,c) let a, b, c be Object of C; ::_thesis: for f, g being Morphism of C st f in H3(a,b) & g in H3(b,c) holds H2(a,b,c,g,f) in H3(a,c) let f, g be Morphism of C; ::_thesis: ( f in H3(a,b) & g in H3(b,c) implies H2(a,b,c,g,f) in H3(a,c) ) assume that A33: f in H3(a,b) and A34: g in H3(b,c) ; ::_thesis: H2(a,b,c,g,f) in H3(a,c) A35: ( cod f = b & dom g = b ) by A33, A34, CAT_1:1; cod g = c by A34, CAT_1:1; then A36: cod (g (*) f) = c by A35, CAT_1:17; dom f = a by A33, CAT_1:1; then dom (g (*) f) = a by A35, CAT_1:17; hence H2(a,b,c,g,f) in H3(a,c) by A36; ::_thesis: verum end; A37: for a, b being Object of C holds H3(a,b) c= the carrier' of C ; consider A being strict MSAlgebra over CatSign the carrier of C such that A38: ( ( for a, b being Element of C holds the Sorts of A . (homsym (a,b)) = H3(a,b) ) & ( for a being Element of C holds (Den ((idsym a),A)) . {} = H1(a) ) ) and A39: for a, b, c being Element of C for f, g being Element of the carrier' of C st f in H3(a,b) & g in H3(b,c) holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = H2(a,b,c,g,f) from CATALG_1:sch_1(A37, A31, A32); take A ; ::_thesis: ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f ) ) now__::_thesis:_for_a,_b,_c_being_Object_of_C for_f,_g_being_Morphism_of_C_st_dom_f_=_a_&_cod_f_=_b_&_dom_g_=_b_&_cod_g_=_c_holds_ (Den_((compsym_(a,b,c)),A))_._<*g,f*>_=_g_(*)_f let a, b, c be Object of C; ::_thesis: for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f let f, g be Morphism of C; ::_thesis: ( dom f = a & cod f = b & dom g = b & cod g = c implies (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f ) assume ( dom f = a & cod f = b & dom g = b & cod g = c ) ; ::_thesis: (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f then ( f in Hom (a,b) & g in Hom (b,c) ) ; hence (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f by A39; ::_thesis: verum end; hence ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f ) ) by A38; ::_thesis: verum end; end; :: deftheorem Def13 defines MSAlg CATALG_1:def_13_:_ for C being Category for b2 being strict MSAlgebra over CatSign the carrier of C holds ( b2 = MSAlg C iff ( ( for a, b being Object of C holds the Sorts of b2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b2)) . {} = id a ) & ( for a, b, c being Object of C for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds (Den ((compsym (a,b,c)),b2)) . <*g,f*> = g (*) f ) ) ); theorem Th25: :: CATALG_1:25 for A being Category for a being Object of A holds Result ((idsym a),(MSAlg A)) = Hom (a,a) proof let A be Category; ::_thesis: for a being Object of A holds Result ((idsym a),(MSAlg A)) = Hom (a,a) let a be Object of A; ::_thesis: Result ((idsym a),(MSAlg A)) = Hom (a,a) thus Result ((idsym a),(MSAlg A)) = the Sorts of (MSAlg A) . (the_result_sort_of (idsym a)) by PRALG_2:3 .= the Sorts of (MSAlg A) . (homsym (a,a)) by Def3 .= Hom (a,a) by Def13 ; ::_thesis: verum end; theorem Th26: :: CATALG_1:26 for A being Category for a, b, c being Object of A holds ( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) ) proof let A be Category; ::_thesis: for a, b, c being Object of A holds ( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) ) let a, b, c be Object of A; ::_thesis: ( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) ) for a, b being Object of A holds the Sorts of (MSAlg A) . (homsym (a,b)) = Hom (a,b) by Def13; hence ( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) ) by Lm3; ::_thesis: verum end; registration let C be Category; cluster MSAlg C -> strict disjoint_valued feasible ; coherence ( MSAlg C is disjoint_valued & MSAlg C is feasible ) proof hereby :: according to PROB_2:def_2,MSAFREE1:def_2 ::_thesis: MSAlg C is feasible let x, y be set ; ::_thesis: ( x <> y implies not the Sorts of (MSAlg C) . x meets the Sorts of (MSAlg C) . y ) assume that A1: x <> y and A2: the Sorts of (MSAlg C) . x meets the Sorts of (MSAlg C) . y ; ::_thesis: contradiction consider z being set such that A3: z in the Sorts of (MSAlg C) . x and A4: z in the Sorts of (MSAlg C) . y by A2, XBOOLE_0:3; dom the Sorts of (MSAlg C) = the carrier of (CatSign the carrier of C) by PARTFUN1:def_2; then reconsider x = x, y = y as SortSymbol of (CatSign the carrier of C) by A3, A4, FUNCT_1:def_2; consider a, b being Object of C such that A5: x = homsym (a,b) by Th14; A6: z in Hom (a,b) by A3, A5, Def13; consider c, d being Object of C such that A7: y = homsym (c,d) by Th14; A8: z in Hom (c,d) by A4, A7, Def13; reconsider z = z as Morphism of C by A6; A9: ( dom z = a & cod z = b ) by A6, CAT_1:1; dom z = c by A8, CAT_1:1; hence contradiction by A1, A5, A7, A8, A9, CAT_1:1; ::_thesis: verum end; let o be OperSymbol of (CatSign the carrier of C); :: according to MSUALG_6:def_1 ::_thesis: ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} ) percases ( o `1 = 1 or o `1 = 2 ) by Th15; suppose o `1 = 1 ; ::_thesis: ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} ) then consider a being Object of C such that A10: o = idsym a by Th16; Result (o,(MSAlg C)) = Hom (a,a) by A10, Th25; hence ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} ) by CAT_1:27; ::_thesis: verum end; suppose o `1 = 2 ; ::_thesis: ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} ) then consider a, b, c being Object of C such that A11: o = compsym (a,b,c) by Th17; set A = the Element of Args (o,(MSAlg C)); assume A12: Args (o,(MSAlg C)) <> {} ; ::_thesis: not Result (o,(MSAlg C)) = {} Args (o,(MSAlg C)) = product <*(Hom (b,c)),(Hom (a,b))*> by A11, Th26; then A13: ex g, f being set st ( g in Hom (b,c) & f in Hom (a,b) & the Element of Args (o,(MSAlg C)) = <*g,f*> ) by A12, FINSEQ_3:124; Result (o,(MSAlg C)) = Hom (a,c) by A11, Th26; hence not Result (o,(MSAlg C)) = {} by A13, CAT_1:24; ::_thesis: verum end; end; end; end; theorem Th27: :: CATALG_1:27 for C1, C2 being Category for F being Functor of C1,C2 holds F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) is ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 holds F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) is ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) let F be Functor of C1,C2; ::_thesis: F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) is ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) set S1 = CatSign the carrier of C1; set S2 = CatSign the carrier of C2; set A1 = MSAlg C1; set A2 = MSAlg C2; set f = Upsilon F; set g = Psi F; set B1 = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)); set H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)); let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in the carrier of (CatSign the carrier of C1) or (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . i is Element of bool [:( the Sorts of (MSAlg C1) . i),( the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . i):] ) assume i in the carrier of (CatSign the carrier of C1) ; ::_thesis: (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . i is Element of bool [:( the Sorts of (MSAlg C1) . i),( the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . i):] then reconsider s = i as SortSymbol of (CatSign the carrier of C1) ; consider a, b being Object of C1 such that A1: s = homsym (a,b) by Th14; Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th23; then the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) = the Sorts of (MSAlg C2) * (Upsilon F) by INSTALG1:def_3; then A2: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . s by FUNCT_2:15; (Upsilon F) . s = homsym ((F . a),(F . b)) by A1, Th20; then A3: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = Hom ((F . a),(F . b)) by Def13; A4: the Sorts of (MSAlg C1) . s = Hom (a,b) by A1, Def13; (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . s = F | ( the Sorts of (MSAlg C1) . s) by Def1; then (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . s = hom (F,a,b) by A4; hence (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . i is Element of bool [:( the Sorts of (MSAlg C1) . i),( the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . i):] by A2, A4, A3; ::_thesis: verum end; theorem Th28: :: CATALG_1:28 for C being Category for a, b, c being Object of C for x being set holds ( x in Args ((compsym (a,b,c)),(MSAlg C)) iff ex g, f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) ) proof let C be Category; ::_thesis: for a, b, c being Object of C for x being set holds ( x in Args ((compsym (a,b,c)),(MSAlg C)) iff ex g, f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) ) let a, b, c be Object of C; ::_thesis: for x being set holds ( x in Args ((compsym (a,b,c)),(MSAlg C)) iff ex g, f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) ) let x be set ; ::_thesis: ( x in Args ((compsym (a,b,c)),(MSAlg C)) iff ex g, f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) ) set A = MSAlg C; for a, b being Object of C holds the Sorts of (MSAlg C) . (homsym (a,b)) = Hom (a,b) by Def13; then A1: Args ((compsym (a,b,c)),(MSAlg C)) = product <*(Hom (b,c)),(Hom (a,b))*> by Lm3; hereby ::_thesis: ( ex g, f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) implies x in Args ((compsym (a,b,c)),(MSAlg C)) ) assume x in Args ((compsym (a,b,c)),(MSAlg C)) ; ::_thesis: ex g, f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) then consider g, f being set such that A2: ( g in Hom (b,c) & f in Hom (a,b) ) and A3: x = <*g,f*> by A1, FINSEQ_3:124; reconsider g = g, f = f as Morphism of C by A2; take g = g; ::_thesis: ex f being Morphism of C st ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) take f = f; ::_thesis: ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) thus x = <*g,f*> by A3; ::_thesis: ( dom f = a & cod f = b & dom g = b & cod g = c ) thus ( dom f = a & cod f = b & dom g = b & cod g = c ) by A2, CAT_1:1; ::_thesis: verum end; given g, f being Morphism of C such that A4: x = <*g,f*> and A5: ( dom f = a & cod f = b & dom g = b & cod g = c ) ; ::_thesis: x in Args ((compsym (a,b,c)),(MSAlg C)) ( f in Hom (a,b) & g in Hom (b,c) ) by A5; hence x in Args ((compsym (a,b,c)),(MSAlg C)) by A1, A4, FINSEQ_3:124; ::_thesis: verum end; theorem Th29: :: CATALG_1:29 for C1, C2 being Category for F being Functor of C1,C2 for a, b, c being Object of C1 for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 for a, b, c being Object of C1 for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> let F be Functor of C1,C2; ::_thesis: for a, b, c being Object of C1 for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> set CS1 = CatSign the carrier of C1; set CS2 = CatSign the carrier of C2; set A1 = MSAlg C1; set A2 = MSAlg C2; set u = Upsilon F; set p = Psi F; set B = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)); let a, b, c be Object of C1; ::_thesis: for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> set o = compsym (a,b,c); let f, g be Morphism of C1; ::_thesis: ( f in Hom (a,b) & g in Hom (b,c) implies for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> ) assume that A1: f in Hom (a,b) and A2: g in Hom (b,c) ; ::_thesis: for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> let x be Element of Args ((compsym (a,b,c)),(MSAlg C1)); ::_thesis: ( x = <*g,f*> implies for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> ) assume A3: x = <*g,f*> ; ::_thesis: for H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) holds H # x = <*(F . g),(F . f)*> F . g in Hom ((F . b),(F . c)) by A2, CAT_1:81; then A4: ( dom (F . g) = F . b & cod (F . g) = F . c ) by CAT_1:1; F . f in Hom ((F . a),(F . b)) by A1, CAT_1:81; then ( dom (F . f) = F . a & cod (F . f) = F . b ) by CAT_1:1; then A5: <*(F . g),(F . f)*> in Args ((compsym ((F . a),(F . b),(F . c))),(MSAlg C2)) by A4, Th28; A6: ( dom g = b & cod g = c ) by A2, CAT_1:1; ( dom f = a & cod f = b ) by A1, CAT_1:1; then A7: x in Args ((compsym (a,b,c)),(MSAlg C1)) by A3, A6, Th28; let H be ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))); ::_thesis: ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) implies H # x = <*(F . g),(F . f)*> ) assume A8: H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) ; ::_thesis: H # x = <*(F . g),(F . f)*> the Sorts of (MSAlg C1) . (homsym (b,c)) = Hom (b,c) by Def13; then H . (homsym (b,c)) = F | (Hom (b,c)) by A8, Def1; then A9: (H . (homsym (b,c))) . g = F . g by A2, FUNCT_1:49; A10: dom <*g,f*> = Seg 2 by FINSEQ_1:89; then A11: 1 in dom <*g,f*> by FINSEQ_1:2, TARSKI:def_2; the Sorts of (MSAlg C1) . (homsym (a,b)) = Hom (a,b) by Def13; then H . (homsym (a,b)) = F | (Hom (a,b)) by A8, Def1; then A12: (H . (homsym (a,b))) . f = F . f by A1, FUNCT_1:49; A13: 2 in dom <*g,f*> by A10, FINSEQ_1:2, TARSKI:def_2; Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th23; then A14: Args ((compsym (a,b,c)),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) = Args (((Psi F) . (compsym (a,b,c))),(MSAlg C2)) by INSTALG1:24 .= Args ((compsym ((F . a),(F . b),(F . c))),(MSAlg C2)) by Th22 ; then consider g9, f9 being Morphism of C2 such that A15: H # x = <*g9,f9*> and dom f9 = F . a and cod f9 = F . b and dom g9 = F . b and cod g9 = F . c by A5, Th28; A16: <*g9,f9*> . 1 = g9 by FINSEQ_1:44; A17: the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> by Def3; then ( <*g,f*> . 1 = g & (the_arity_of (compsym (a,b,c))) /. 1 = homsym (b,c) ) by FINSEQ_1:44, FINSEQ_4:17; then A18: <*g9,f9*> . 1 = F . g by A3, A7, A5, A14, A15, A9, A11, MSUALG_3:24; ( <*g,f*> . 2 = f & (the_arity_of (compsym (a,b,c))) /. 2 = homsym (a,b) ) by A17, FINSEQ_1:44, FINSEQ_4:17; then <*g9,f9*> . 2 = F . f by A3, A7, A5, A14, A15, A12, A13, MSUALG_3:24; hence H # x = <*(F . g),(F . f)*> by A15, A18, A16, FINSEQ_1:44; ::_thesis: verum end; theorem Th30: :: CATALG_1:30 for C being Category for a, b, c being Object of C for f, g being Morphism of C st f in Hom (a,b) & g in Hom (b,c) holds (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f proof let C be Category; ::_thesis: for a, b, c being Object of C for f, g being Morphism of C st f in Hom (a,b) & g in Hom (b,c) holds (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f let a, b, c be Object of C; ::_thesis: for f, g being Morphism of C st f in Hom (a,b) & g in Hom (b,c) holds (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f let f, g be Morphism of C; ::_thesis: ( f in Hom (a,b) & g in Hom (b,c) implies (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f ) assume that A1: f in Hom (a,b) and A2: g in Hom (b,c) ; ::_thesis: (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f A3: ( dom g = b & cod g = c ) by A2, CAT_1:1; ( dom f = a & cod f = b ) by A1, CAT_1:1; hence (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f by A3, Def13; ::_thesis: verum end; theorem :: CATALG_1:31 for C being Category for a, b, c, d being Object of C for f, g, h being Morphism of C st f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) holds (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> proof let C be Category; ::_thesis: for a, b, c, d being Object of C for f, g, h being Morphism of C st f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) holds (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> let a, b, c, d be Object of C; ::_thesis: for f, g, h being Morphism of C st f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) holds (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> let f, g, h be Morphism of C; ::_thesis: ( f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) implies (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> ) assume that A1: f in Hom (a,b) and A2: g in Hom (b,c) and A3: h in Hom (c,d) ; ::_thesis: (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> A4: cod g = c by A2, CAT_1:1; A5: (Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*> = h (*) g by A2, A3, Th30; A6: cod f = b by A1, CAT_1:1; A7: dom h = c by A3, CAT_1:1; cod h = d by A3, CAT_1:1; then A8: cod (h (*) g) = d by A4, A7, CAT_1:17; A9: dom g = b by A2, CAT_1:1; then dom (h (*) g) = b by A4, A7, CAT_1:17; then A10: h (*) g in Hom (b,d) by A8; dom f = a by A1, CAT_1:1; then A11: dom (g (*) f) = a by A6, A9, CAT_1:17; cod (g (*) f) = c by A6, A9, A4, CAT_1:17; then A12: g (*) f in Hom (a,c) by A11; (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f by A1, A2, Th30; hence (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = h (*) (g (*) f) by A3, A12, Th30 .= (h (*) g) (*) f by A6, A9, A4, A7, CAT_1:18 .= (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> by A1, A5, A10, Th30 ; ::_thesis: verum end; theorem :: CATALG_1:32 for C being Category for a, b being Object of C for f being Morphism of C st f in Hom (a,b) holds ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) proof let C be Category; ::_thesis: for a, b being Object of C for f being Morphism of C st f in Hom (a,b) holds ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) let a, b be Object of C; ::_thesis: for f being Morphism of C st f in Hom (a,b) holds ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) let f be Morphism of C; ::_thesis: ( f in Hom (a,b) implies ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) ) assume A1: f in Hom (a,b) ; ::_thesis: ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) then dom f = a by CAT_1:1; then A2: f (*) (id a) = f by CAT_1:22; cod f = b by A1, CAT_1:1; then A3: (id b) (*) f = f by CAT_1:21; ( id b in Hom (b,b) & id a in Hom (a,a) ) by CAT_1:27; hence ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) by A1, A3, A2, Th30; ::_thesis: verum end; theorem :: CATALG_1:33 for C1, C2 being Category for F being Functor of C1,C2 ex H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) ) proof let C1, C2 be Category; ::_thesis: for F being Functor of C1,C2 ex H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) ) let F be Functor of C1,C2; ::_thesis: ex H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) ) set S1 = CatSign the carrier of C1; set S2 = CatSign the carrier of C2; set A1 = MSAlg C1; set A2 = MSAlg C2; set f = Upsilon F; set G = Psi F; set B1 = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)); A1: Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th23; reconsider H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) as ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) by Th27; take H ; ::_thesis: ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) ) thus H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) ; ::_thesis: H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) let o be OperSymbol of (CatSign the carrier of C1); :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(MSAlg C1)) = {} or for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1) ) assume A2: Args (o,(MSAlg C1)) <> {} ; ::_thesis: for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1) percases ( o `1 = 1 or o `1 = 2 ) by Th15; suppose o `1 = 1 ; ::_thesis: for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1) then consider a being Object of C1 such that A3: o = idsym a by Th16; let x be Element of Args (o,(MSAlg C1)); ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) A4: Args (((Psi F) . o),(MSAlg C2)) = Args (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) by A1, INSTALG1:24; A5: (Psi F) . o = idsym (F . a) by A3, Th21; then Args (((Psi F) . o),(MSAlg C2)) = {{}} by Th24; then A6: H # x = {} by A4, TARSKI:def_1; reconsider h = id a as Morphism of a,a ; ( dom (id a) = a & cod (id a) = a ) by CAT_1:58; then A7: id a in Hom (a,a) ; Args (o,(MSAlg C1)) = {{}} by A3, Th24; then x = {} by TARSKI:def_1; hence (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (H . (the_result_sort_of o)) . h by A3, Def13 .= (H . (homsym (a,a))) . h by A3, Def3 .= (F | ( the Sorts of (MSAlg C1) . (homsym (a,a)))) . h by Def1 .= (F | (Hom (a,a))) . h by Def13 .= (hom (F,a,a)) . h .= F . h by A7, CAT_1:88 .= id (F . a) by CAT_1:71 .= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A5, A6, Def13 .= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th23, INSTALG1:23 ; ::_thesis: verum end; supposeA8: o `1 = 2 ; ::_thesis: for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1) let x be Element of Args (o,(MSAlg C1)); ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) consider a, b, c being Object of C1 such that A9: o = compsym (a,b,c) by A8, Th17; A10: (Psi F) . o = compsym ((F . a),(F . b),(F . c)) by A9, Th22; consider g, h being Morphism of C1 such that A11: x = <*g,h*> and A12: dom h = a and A13: cod h = b and A14: dom g = b and A15: cod g = c by A2, A9, Th28; A16: ( g in Hom (b,c) & h in Hom (a,b) ) by A12, A13, A14, A15; ( dom (g (*) h) = a & cod (g (*) h) = c ) by A12, A13, A14, A15, CAT_1:17; then A17: g (*) h in Hom (a,c) ; then reconsider gh = g (*) h as Morphism of a,c by CAT_1:def_5; A18: ( dom (F . h) = F . a & cod (F . h) = F . b ) by A12, A13, CAT_1:72; A19: ( dom (F . g) = F . b & cod (F . g) = F . c ) by A14, A15, CAT_1:72; thus (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (H . (the_result_sort_of o)) . gh by A9, A11, A12, A13, A14, A15, Def13 .= (H . (homsym (a,c))) . gh by A9, Def3 .= (F | ( the Sorts of (MSAlg C1) . (homsym (a,c)))) . gh by Def1 .= (F | (Hom (a,c))) . gh by Def13 .= (hom (F,a,c)) . gh .= F . gh by A17, CAT_1:88 .= (F . g) (*) (F . h) by A13, A14, CAT_1:64 .= (Den (((Psi F) . o),(MSAlg C2))) . <*(F . g),(F . h)*> by A10, A18, A19, Def13 .= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A9, A11, A16, Th29 .= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th23, INSTALG1:23 ; ::_thesis: verum end; end; end;