:: MSINST_1 semantic presentation begin definition let A be non empty set ; func MSSCat A -> non empty strict AltCatStr means :Def1: :: MSINST_1:def 1 ( the carrier of it = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of it . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of it st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of it . (i,j) & [g1,g2] in the Arrows of it . (j,k) holds ( the Comp of it . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ); existence ex b1 being non empty strict AltCatStr st ( the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds ( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) proof set c = MSS_set A; deffunc H1( Element of MSS_set A, Element of MSS_set A) -> set = MSS_morph ($1,$2); consider M being ManySortedSet of [:(MSS_set A),(MSS_set A):] such that A1: for i, j being Element of MSS_set A holds M . (i,j) = H1(i,j) from ALTCAT_1:sch_2(); defpred S1[ set , set , set ] means ex i, j, k being Element of MSS_set A st ( $3 = [i,j,k] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (i,j) & [g1,g2] in M . (j,k) & $2 = [[g1,g2],[f1,f2]] holds $1 = [(g1 * f1),(g2 * f2)] ) ); A2: for ijk being set st ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] holds for x being set st x in {|M,M|} . ijk holds ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) proof let ijk be set ; ::_thesis: ( ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] implies for x being set st x in {|M,M|} . ijk holds ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) ) assume ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] ; ::_thesis: for x being set st x in {|M,M|} . ijk holds ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) then consider x1, x2, x3 being set such that A3: ( x1 in MSS_set A & x2 in MSS_set A & x3 in MSS_set A ) and A4: ijk = [x1,x2,x3] by MCART_1:68; reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSS_set A by A3; let x be set ; ::_thesis: ( x in {|M,M|} . ijk implies ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) ) A5: ( {|M,M|} . (x1,x2,x3) = {|M,M|} . [x1,x2,x3] & {|M,M|} . (x1,x2,x3) = [:(M . (x2,x3)),(M . (x1,x2)):] ) by ALTCAT_1:def_4, MULTOP_1:def_1; A6: {|M|} . ijk = {|M|} . (x1,x2,x3) by A4, MULTOP_1:def_1; assume A7: x in {|M,M|} . ijk ; ::_thesis: ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) then x `1 in M . (x2,x3) by A4, A5, MCART_1:10; then x `1 in MSS_morph (x2,x3) by A1; then consider g1, g2 being Function such that A8: x `1 = [g1,g2] and A9: g1,g2 form_morphism_between x2,x3 by MSALIMIT:def_10; x `2 in M . (x1,x2) by A4, A7, A5, MCART_1:10; then x `2 in MSS_morph (x1,x2) by A1; then consider f1, f2 being Function such that A10: x `2 = [f1,f2] and A11: f1,f2 form_morphism_between x1,x2 by MSALIMIT:def_10; take y = [(g1 * f1),(g2 * f2)]; ::_thesis: ( y in {|M|} . ijk & S1[y,x,ijk] ) g1 * f1,g2 * f2 form_morphism_between x1,x3 by A11, A9, PUA2MSS1:29; then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSS_morph (x1,x3) ) by ALTCAT_1:def_3, MSALIMIT:def_10; hence y in {|M|} . ijk by A1, A6; ::_thesis: S1[y,x,ijk] take x1 ; ::_thesis: ex j, k being Element of MSS_set A st ( ijk = [x1,j,k] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,j) & [g1,g2] in M . (j,k) & x = [[g1,g2],[f1,f2]] holds y = [(g1 * f1),(g2 * f2)] ) ) take x2 ; ::_thesis: ex k being Element of MSS_set A st ( ijk = [x1,x2,k] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,x2) & [g1,g2] in M . (x2,k) & x = [[g1,g2],[f1,f2]] holds y = [(g1 * f1),(g2 * f2)] ) ) take x3 ; ::_thesis: ( ijk = [x1,x2,x3] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,x2) & [g1,g2] in M . (x2,x3) & x = [[g1,g2],[f1,f2]] holds y = [(g1 * f1),(g2 * f2)] ) ) thus ijk = [x1,x2,x3] by A4; ::_thesis: for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,x2) & [g1,g2] in M . (x2,x3) & x = [[g1,g2],[f1,f2]] holds y = [(g1 * f1),(g2 * f2)] let F1, F2, G1, G2 be Function; ::_thesis: ( [F1,F2] in M . (x1,x2) & [G1,G2] in M . (x2,x3) & x = [[G1,G2],[F1,F2]] implies y = [(G1 * F1),(G2 * F2)] ) assume that [F1,F2] in M . (x1,x2) and [G1,G2] in M . (x2,x3) and A12: x = [[G1,G2],[F1,F2]] ; ::_thesis: y = [(G1 * F1),(G2 * F2)] x `1 = [G1,G2] by A12, MCART_1:7; then A13: ( G1 = g1 & G2 = g2 ) by A8, XTUPLE_0:1; A14: x `2 = [F1,F2] by A12, MCART_1:7; then F1 = f1 by A10, XTUPLE_0:1; hence y = [(G1 * F1),(G2 * F2)] by A10, A14, A13, XTUPLE_0:1; ::_thesis: verum end; consider F being ManySortedFunction of {|M,M|},{|M|} such that A15: for ijk being set st ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] holds ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st ( f = F . ijk & ( for x being set st x in {|M,M|} . ijk holds S1[f . x,x,ijk] ) ) from MSSUBFAM:sch_1(A2); take EX = AltCatStr(# (MSS_set A),M,F #); ::_thesis: ( the carrier of EX = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of EX . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of EX st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) reconsider EX = EX as non empty AltCatStr ; for i, j, k being object of EX st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] proof let i, j, k be object of EX; ::_thesis: ( i in MSS_set A & j in MSS_set A & k in MSS_set A implies for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) assume that i in MSS_set A and j in MSS_set A and k in MSS_set A ; ::_thesis: for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] let f1, f2, g1, g2 be Function; ::_thesis: ( [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) assume A16: ( [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) ) ; ::_thesis: ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] set x = [[g1,g2],[f1,f2]]; set ijk = [i,j,k]; [i,j,k] in [:(MSS_set A),(MSS_set A),(MSS_set A):] by MCART_1:69; then consider f being Function of ({|M,M|} . [i,j,k]),({|M|} . [i,j,k]) such that A17: f = F . [i,j,k] and A18: for x being set st x in {|M,M|} . [i,j,k] holds S1[f . x,x,[i,j,k]] by A15; A19: f = the Comp of EX . (i,j,k) by A17, MULTOP_1:def_1; ( {|M,M|} . (i,j,k) = {|M,M|} . [i,j,k] & {|M,M|} . (i,j,k) = [:(M . (j,k)),(M . (i,j)):] ) by ALTCAT_1:def_4, MULTOP_1:def_1; then [[g1,g2],[f1,f2]] in {|M,M|} . [i,j,k] by A16, ZFMISC_1:87; then consider I, J, K being Element of MSS_set A such that A20: [i,j,k] = [I,J,K] and A21: for f1, f2, g1, g2 being Function st [f1,f2] in M . (I,J) & [g1,g2] in M . (J,K) & [[g1,g2],[f1,f2]] = [[g1,g2],[f1,f2]] holds f . [[g1,g2],[f1,f2]] = [(g1 * f1),(g2 * f2)] by A18; A22: K = k by A20, XTUPLE_0:3; ( I = i & J = j ) by A20, XTUPLE_0:3; hence ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] by A16, A21, A22, A19; ::_thesis: verum end; hence ( the carrier of EX = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of EX . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of EX st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds ( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds ( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) holds b1 = b2 proof set c = MSS_set A; let A1, A2 be non empty strict AltCatStr ; ::_thesis: ( the carrier of A1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of A1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds ( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of A2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of A2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds ( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) implies A1 = A2 ) assume that A23: the carrier of A1 = MSS_set A and A24: for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) and A25: for i, j, k being object of A1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds ( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] and A26: the carrier of A2 = MSS_set A and A27: for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) and A28: for i, j, k being object of A2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds ( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ; ::_thesis: A1 = A2 reconsider AA2 = the Arrows of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A26; reconsider AA1 = the Arrows of A1 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A23; reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A),(MSS_set A):] by A23, A26; A29: now__::_thesis:_for_i,_j_being_Element_of_MSS_set_A_holds_AA1_._(i,j)_=_AA2_._(i,j) let i, j be Element of MSS_set A; ::_thesis: AA1 . (i,j) = AA2 . (i,j) thus AA1 . (i,j) = MSS_morph (i,j) by A24 .= AA2 . (i,j) by A27 ; ::_thesis: verum end; then A30: AA1 = AA2 by ALTCAT_1:7; now__::_thesis:_for_i,_j,_k_being_set_st_i_in_MSS_set_A_&_j_in_MSS_set_A_&_k_in_MSS_set_A_holds_ CC1_._(i,j,k)_=_CC2_._(i,j,k) let i, j, k be set ; ::_thesis: ( i in MSS_set A & j in MSS_set A & k in MSS_set A implies CC1 . (i,j,k) = CC2 . (i,j,k) ) set ijk = [i,j,k]; A31: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def_1; assume A32: ( i in MSS_set A & j in MSS_set A & k in MSS_set A ) ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k) then reconsider i9 = i, j9 = j, k9 = k as Element of MSS_set A ; reconsider I9 = i, J9 = j, K9 = k as Element of A2 by A26, A32; reconsider I = i, J = j, K = k as Element of A1 by A23, A32; A33: [i,j,k] in [:(MSS_set A),(MSS_set A),(MSS_set A):] by A32, MCART_1:69; A34: CC2 . (i,j,k) = CC2 . [i,j,k] by MULTOP_1:def_1; thus CC1 . (i,j,k) = CC2 . (i,j,k) ::_thesis: verum proof reconsider Cj = CC2 . [i,j,k] as Function of ({|AA2,AA2|} . [i,j,k]),({|AA2|} . [i,j,k]) by A26, A33, PBOOLE:def_15; reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A23, A33, PBOOLE:def_15; percases ( {|AA1|} . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} ) ; supposeA35: {|AA1|} . [i,j,k] <> {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k) A36: for x being set st x in {|AA1,AA1|} . [i,j,k] holds Ci . x = Cj . x proof let x be set ; ::_thesis: ( x in {|AA1,AA1|} . [i,j,k] implies Ci . x = Cj . x ) assume A37: x in {|AA1,AA1|} . [i,j,k] ; ::_thesis: Ci . x = Cj . x then x in {|AA1,AA1|} . (i,j,k) by MULTOP_1:def_1; then A38: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A32, ALTCAT_1:def_4; then A39: x `1 in AA1 . (j,k) by MCART_1:10; then x `1 in MSS_morph (j9,k9) by A24; then consider g1, g2 being Function such that A40: x `1 = [g1,g2] and g1,g2 form_morphism_between j9,k9 by MSALIMIT:def_10; x in {|AA2,AA2|} . (i,j,k) by A30, A37, MULTOP_1:def_1; then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A32, ALTCAT_1:def_4; then A41: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10; A42: x `2 in AA1 . (i,j) by A38, MCART_1:10; then x `2 in MSS_morph (i9,j9) by A24; then consider f1, f2 being Function such that A43: x `2 = [f1,f2] and f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10; A44: x = [[g1,g2],[f1,f2]] by A38, A40, A43, MCART_1:21; then Ci . x = ( the Comp of A1 . (I,J,K)) . ([g1,g2],[f1,f2]) by MULTOP_1:def_1 .= [(g1 * f1),(g2 * f2)] by A23, A25, A39, A42, A40, A43 .= ( the Comp of A2 . (I9,J9,K9)) . ([g1,g2],[f1,f2]) by A26, A28, A41, A40, A43 .= Cj . x by A44, MULTOP_1:def_1 ; hence Ci . x = Cj . x ; ::_thesis: verum end; {|AA2|} . [i,j,k] <> {} by A29, A35, ALTCAT_1:7; then A45: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def_1; dom Ci = {|AA1,AA1|} . [i,j,k] by A35, FUNCT_2:def_1; hence CC1 . (i,j,k) = CC2 . (i,j,k) by A30, A31, A34, A45, A36, FUNCT_1:2; ::_thesis: verum end; suppose {|AA1|} . [i,j,k] = {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k) then ( Ci = {} & Cj = {} ) by A30; hence CC1 . (i,j,k) = CC2 . (i,j,k) by A31, MULTOP_1:def_1; ::_thesis: verum end; end; end; end; hence A1 = A2 by A23, A26, A30, ALTCAT_1:8; ::_thesis: verum end; end; :: deftheorem Def1 defines MSSCat MSINST_1:def_1_:_ for A being non empty set for b2 being non empty strict AltCatStr holds ( b2 = MSSCat A iff ( the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds ( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) ); registration let A be non empty set ; cluster MSSCat A -> non empty transitive strict associative with_units ; coherence ( MSSCat A is transitive & MSSCat A is associative & MSSCat A is with_units ) proof set M = MSSCat A; set G = MSSCat A; thus MSSCat A is transitive ::_thesis: ( MSSCat A is associative & MSSCat A is with_units ) proof let o1, o2, o3 be object of (MSSCat A); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) reconsider o19 = o1, o29 = o2, o39 = o3 as Element of MSS_set A by Def1; assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {} set s = the Element of MSS_morph (o29,o39); MSS_morph (o29,o39) <> {} by A2, Def1; then consider u, w being Function such that the Element of MSS_morph (o29,o39) = [u,w] and A3: u,w form_morphism_between o29,o39 by MSALIMIT:def_10; set t = the Element of MSS_morph (o19,o29); MSS_morph (o19,o29) <> {} by A1, Def1; then consider f, g being Function such that the Element of MSS_morph (o19,o29) = [f,g] and A4: f,g form_morphism_between o19,o29 by MSALIMIT:def_10; u * f,w * g form_morphism_between o19,o39 by A4, A3, PUA2MSS1:29; then [(u * f),(w * g)] in MSS_morph (o19,o39) by MSALIMIT:def_10; hence not <^o1,o3^> = {} by Def1; ::_thesis: verum end; set G = the Arrows of (MSSCat A); set C = the Comp of (MSSCat A); thus the Comp of (MSSCat A) is associative :: according to ALTCAT_1:def_15 ::_thesis: MSSCat A is with_units proof let i, j, k, l be Element of (MSSCat A); :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds ( not b1 in the Arrows of (MSSCat A) . (i,j) or not b2 in the Arrows of (MSSCat A) . (j,k) or not b3 in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (b3,(( the Comp of (MSSCat A) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (b3,b2)),b1) ) reconsider I = i, J = j, K = k, L = l as object of (MSSCat A) ; let f, g, h be set ; ::_thesis: ( not f in the Arrows of (MSSCat A) . (i,j) or not g in the Arrows of (MSSCat A) . (j,k) or not h in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f) ) reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of MSS_set A by Def1; assume that A5: f in the Arrows of (MSSCat A) . (i,j) and A6: g in the Arrows of (MSSCat A) . (j,k) and A7: h in the Arrows of (MSSCat A) . (k,l) ; ::_thesis: ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f) g in MSS_morph (j9,k9) by A6, Def1; then consider g1, g2 being Function such that A8: g = [g1,g2] and A9: g1,g2 form_morphism_between j9,k9 by MSALIMIT:def_10; f in MSS_morph (i9,j9) by A5, Def1; then consider f1, f2 being Function such that A10: f = [f1,f2] and A11: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10; A12: ( the Comp of (MSSCat A) . (i,j,k)) . (g,f) = [(g1 * f1),(g2 * f2)] by A5, A6, A10, A11, A8, A9, Def1; h in MSS_morph (k9,l9) by A7, Def1; then consider h1, h2 being Function such that A13: h = [h1,h2] and A14: h1,h2 form_morphism_between k9,l9 by MSALIMIT:def_10; A15: ( the Comp of (MSSCat A) . (j,k,l)) . (h,g) = [(h1 * g1),(h2 * g2)] by A6, A7, A8, A9, A13, A14, Def1; h1 * g1,h2 * g2 form_morphism_between j9,l9 by A9, A14, PUA2MSS1:29; then [(h1 * g1),(h2 * g2)] in MSS_morph (j9,l9) by MSALIMIT:def_10; then A16: [(h1 * g1),(h2 * g2)] in the Arrows of (MSSCat A) . (j,l) by Def1; A17: ( (h1 * g1) * f1 = h1 * (g1 * f1) & (h2 * g2) * f2 = h2 * (g2 * f2) ) by RELAT_1:36; J in the carrier of (MSSCat A) ; then A18: J in MSS_set A by Def1; L in the carrier of (MSSCat A) ; then A19: L in MSS_set A by Def1; g1 * f1,g2 * f2 form_morphism_between i9,k9 by A11, A9, PUA2MSS1:29; then [(g1 * f1),(g2 * f2)] in MSS_morph (i9,k9) by MSALIMIT:def_10; then A20: [(g1 * f1),(g2 * f2)] in the Arrows of (MSSCat A) . (i,k) by Def1; I in the carrier of (MSSCat A) ; then A21: I in MSS_set A by Def1; K in the carrier of (MSSCat A) ; then K in MSS_set A by Def1; then ( the Comp of (MSSCat A) . (i,k,l)) . (h,[(g1 * f1),(g2 * f2)]) = [(h1 * (g1 * f1)),(h2 * (g2 * f2))] by A21, A19, A7, A13, A20, Def1; hence ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f) by A21, A18, A19, A5, A10, A12, A15, A16, A17, Def1; ::_thesis: verum end; thus the Comp of (MSSCat A) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (MSSCat A) is with_right_units proof let j be Element of (MSSCat A); :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st ( b1 in the Arrows of (MSSCat A) . (j,j) & ( for b2 being Element of the carrier of (MSSCat A) for b3 being set holds ( not b3 in the Arrows of (MSSCat A) . (b2,j) or ( the Comp of (MSSCat A) . (b2,j,j)) . (b1,b3) = b3 ) ) ) reconsider j9 = j as Element of MSS_set A by Def1; set e1 = id the carrier of j9; set e2 = id the carrier' of j9; take e = [(id the carrier of j9),(id the carrier' of j9)]; ::_thesis: ( e in the Arrows of (MSSCat A) . (j,j) & ( for b1 being Element of the carrier of (MSSCat A) for b2 being set holds ( not b2 in the Arrows of (MSSCat A) . (b1,j) or ( the Comp of (MSSCat A) . (b1,j,j)) . (e,b2) = b2 ) ) ) ( id the carrier of j9, id the carrier' of j9 form_morphism_between j9,j9 & the Arrows of (MSSCat A) . (j,j) = MSS_morph (j9,j9) ) by Def1, PUA2MSS1:28; hence A22: e in the Arrows of (MSSCat A) . (j,j) by MSALIMIT:def_10; ::_thesis: for b1 being Element of the carrier of (MSSCat A) for b2 being set holds ( not b2 in the Arrows of (MSSCat A) . (b1,j) or ( the Comp of (MSSCat A) . (b1,j,j)) . (e,b2) = b2 ) let i be Element of (MSSCat A); ::_thesis: for b1 being set holds ( not b1 in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,b1) = b1 ) reconsider i9 = i as Element of MSS_set A by Def1; let f be set ; ::_thesis: ( not f in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f ) reconsider I = i, J = j as object of (MSSCat A) ; assume A23: f in the Arrows of (MSSCat A) . (i,j) ; ::_thesis: ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f then f in MSS_morph (i9,j9) by Def1; then consider f1, f2 being Function such that A24: f = [f1,f2] and A25: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10; A26: rng f2 c= the carrier' of j9 by A25, PUA2MSS1:def_12; rng f1 c= the carrier of j9 by A25, PUA2MSS1:def_12; then A27: (id the carrier of j9) * f1 = f1 by RELAT_1:53; ( the Comp of (MSSCat A) . (I,J,J)) . ([(id the carrier of j9),(id the carrier' of j9)],[f1,f2]) = [((id the carrier of j9) * f1),((id the carrier' of j9) * f2)] by A22, A23, A24, A25, Def1; hence ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f by A24, A26, A27, RELAT_1:53; ::_thesis: verum end; thus the Comp of (MSSCat A) is with_right_units ::_thesis: verum proof let i be Element of (MSSCat A); :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st ( b1 in the Arrows of (MSSCat A) . (i,i) & ( for b2 being Element of the carrier of (MSSCat A) for b3 being set holds ( not b3 in the Arrows of (MSSCat A) . (i,b2) or ( the Comp of (MSSCat A) . (i,i,b2)) . (b3,b1) = b3 ) ) ) reconsider i9 = i as Element of MSS_set A by Def1; set e1 = id the carrier of i9; set e2 = id the carrier' of i9; take e = [(id the carrier of i9),(id the carrier' of i9)]; ::_thesis: ( e in the Arrows of (MSSCat A) . (i,i) & ( for b1 being Element of the carrier of (MSSCat A) for b2 being set holds ( not b2 in the Arrows of (MSSCat A) . (i,b1) or ( the Comp of (MSSCat A) . (i,i,b1)) . (b2,e) = b2 ) ) ) ( id the carrier of i9, id the carrier' of i9 form_morphism_between i9,i9 & the Arrows of (MSSCat A) . (i,i) = MSS_morph (i9,i9) ) by Def1, PUA2MSS1:28; hence A28: e in the Arrows of (MSSCat A) . (i,i) by MSALIMIT:def_10; ::_thesis: for b1 being Element of the carrier of (MSSCat A) for b2 being set holds ( not b2 in the Arrows of (MSSCat A) . (i,b1) or ( the Comp of (MSSCat A) . (i,i,b1)) . (b2,e) = b2 ) let j be Element of (MSSCat A); ::_thesis: for b1 being set holds ( not b1 in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (b1,e) = b1 ) reconsider j9 = j as Element of MSS_set A by Def1; let f be set ; ::_thesis: ( not f in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f ) reconsider I = i, J = j as object of (MSSCat A) ; assume A29: f in the Arrows of (MSSCat A) . (i,j) ; ::_thesis: ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f then f in MSS_morph (i9,j9) by Def1; then consider f1, f2 being Function such that A30: f = [f1,f2] and A31: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10; A32: dom f2 = the carrier' of i9 by A31, PUA2MSS1:def_12; dom f1 = the carrier of i9 by A31, PUA2MSS1:def_12; then A33: f1 * (id the carrier of i9) = f1 by RELAT_1:52; ( the Comp of (MSSCat A) . (I,I,J)) . ([f1,f2],[(id the carrier of i9),(id the carrier' of i9)]) = [(f1 * (id the carrier of i9)),(f2 * (id the carrier' of i9))] by A28, A29, A30, A31, Def1; hence ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f by A30, A32, A33, RELAT_1:52; ::_thesis: verum end; end; end; theorem :: MSINST_1:1 for A being non empty set for C being category st C = MSSCat A holds for o being object of C holds o is non empty non void ManySortedSign proof let A be non empty set ; ::_thesis: for C being category st C = MSSCat A holds for o being object of C holds o is non empty non void ManySortedSign let C be category; ::_thesis: ( C = MSSCat A implies for o being object of C holds o is non empty non void ManySortedSign ) assume A1: C = MSSCat A ; ::_thesis: for o being object of C holds o is non empty non void ManySortedSign let o be object of C; ::_thesis: o is non empty non void ManySortedSign reconsider o = o as Element of MSS_set A by A1, Def1; o is non empty non void ManySortedSign ; hence o is non empty non void ManySortedSign ; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; cluster strict feasible for MSAlgebra over S; existence ex b1 being MSAlgebra over S st ( b1 is strict & b1 is feasible ) proof set M = the feasible MSAlgebra over S; take E = MSAlgebra(# the Sorts of the feasible MSAlgebra over S, the Charact of the feasible MSAlgebra over S #); ::_thesis: ( E is strict & E is feasible ) thus E is strict ; ::_thesis: E is feasible now__::_thesis:_for_o_being_OperSymbol_of_S_st_Args_(o,E)_<>_{}_holds_ Result_(o,E)_<>_{} let o be OperSymbol of S; ::_thesis: ( Args (o,E) <> {} implies Result (o,E) <> {} ) A1: Args (o, the feasible MSAlgebra over S) = (( the Sorts of E #) * the Arity of S) . o by MSUALG_1:def_4 .= Args (o,E) by MSUALG_1:def_4 ; Result (o, the feasible MSAlgebra over S) = ( the Sorts of E * the ResultSort of S) . o by MSUALG_1:def_5 .= Result (o,E) by MSUALG_1:def_5 ; hence ( Args (o,E) <> {} implies Result (o,E) <> {} ) by A1, MSUALG_6:def_1; ::_thesis: verum end; hence E is feasible by MSUALG_6:def_1; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let A be non empty set ; func MSAlg_set (S,A) -> set means :Def2: :: MSINST_1:def 2 for x being set holds ( x in it iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) proof defpred S1[ set , set ] means ex M being strict feasible MSAlgebra over S st ( M = $2 & $1 = [ the Sorts of M, the Charact of M] ); A1: for x, y, z being set st S1[x,y] & S1[x,z] holds y = z proof let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[x,z] implies y = z ) given M being strict feasible MSAlgebra over S such that A2: M = y and A3: x = [ the Sorts of M, the Charact of M] ; ::_thesis: ( not S1[x,z] or y = z ) given N being strict feasible MSAlgebra over S such that A4: N = z and A5: x = [ the Sorts of N, the Charact of N] ; ::_thesis: y = z the Sorts of M = the Sorts of N by A3, A5, XTUPLE_0:1; hence y = z by A2, A3, A4, A5, XTUPLE_0:1; ::_thesis: verum end; consider X being set such that A6: for x being set holds ( x in X iff ex y being set st ( y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] & S1[y,x] ) ) from TARSKI:sch_1(A1); take X ; ::_thesis: for x being set holds ( x in X iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) thus for x being set holds ( x in X iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ::_thesis: verum proof let x be set ; ::_thesis: ( x in X iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) hereby ::_thesis: ( ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) implies x in X ) assume x in X ; ::_thesis: ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) then consider y being set such that A7: y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] and A8: S1[y,x] by A6; consider M being strict feasible MSAlgebra over S such that A9: M = x and y = [ the Sorts of M, the Charact of M] by A8; take M = M; ::_thesis: ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) thus x = M by A9; ::_thesis: for C being Component of the Sorts of M holds C c= A thus for C being Component of the Sorts of M holds C c= A ::_thesis: verum proof let C be Component of the Sorts of M; ::_thesis: C c= A consider y1 being set such that y1 in dom the Sorts of M and A10: C = the Sorts of M . y1 by FUNCT_1:def_3; the Sorts of M in Funcs ( the carrier of S,(bool A)) by A7, A8, A9, ZFMISC_1:87; then consider f being Function such that A11: the Sorts of M = f and dom f = the carrier of S and A12: rng f c= bool A by FUNCT_2:def_2; f . y1 in rng f by A10, A11; hence C c= A by A10, A11, A12; ::_thesis: verum end; end; given M being strict feasible MSAlgebra over S such that A13: x = M and A14: for C being Component of the Sorts of M holds C c= A ; ::_thesis: x in X A15: dom the Sorts of M = the carrier of S by PARTFUN1:def_2; then reconsider SM = the Sorts of M as Function of the carrier of S,(rng the Sorts of M) by FUNCT_2:1; A16: rng the Sorts of M c= bool A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of M or x in bool A ) assume x in rng the Sorts of M ; ::_thesis: x in bool A then reconsider x9 = x as Component of the Sorts of M ; x9 c= A by A14; hence x in bool A ; ::_thesis: verum end; then reconsider SM9 = SM as Function of the carrier of S,(bool A) by FUNCT_2:6; consider y being set such that A17: y = [ the Sorts of M, the Charact of M] ; A18: dom the Charact of M = the carrier' of S by PARTFUN1:def_2; rng the Charact of M c= PFuncs ((PFuncs (NAT,A)),A) proof reconsider SA = ( the Sorts of M #) * the Arity of S, SR = the Sorts of M * the ResultSort of S as ManySortedSet of the carrier' of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Charact of M or x in PFuncs ((PFuncs (NAT,A)),A) ) reconsider CM = the Charact of M as ManySortedFunction of SA,SR ; assume x in rng the Charact of M ; ::_thesis: x in PFuncs ((PFuncs (NAT,A)),A) then consider x1 being set such that A19: x1 in dom the Charact of M and A20: x = the Charact of M . x1 by FUNCT_1:def_3; reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A19, PBOOLE:def_15; A21: x1 in dom SA by A18, A19, PARTFUN1:def_2; SA . x1 c= PFuncs (NAT,A) proof reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A19, FUNCT_2:5; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SA . x1 or a in PFuncs (NAT,A) ) assume a in SA . x1 ; ::_thesis: a in PFuncs (NAT,A) then A22: a in ( the Sorts of M #) . ( the Arity of S . x1) by A21, FUNCT_1:12; ( the Sorts of M #) . AX = product ( the Sorts of M * AX) by FINSEQ_2:def_5; then A23: ex g being Function st ( a = g & dom g = dom ( the Sorts of M * AX) & ( for x2 being set st x2 in dom ( the Sorts of M * AX) holds g . x2 in ( the Sorts of M * AX) . x2 ) ) by A22, CARD_3:def_5; then reconsider a9 = a as Function ; rng AX c= dom the Sorts of M by A15; then A24: dom a9 = dom AX by A23, RELAT_1:27; rng a9 c= A proof rng the Sorts of M c= bool A proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng the Sorts of M or w in bool A ) assume w in rng the Sorts of M ; ::_thesis: w in bool A then reconsider w9 = w as Component of the Sorts of M ; w9 c= A by A14; hence w in bool A ; ::_thesis: verum end; then A25: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:77; let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng a9 or r in A ) assume r in rng a9 ; ::_thesis: r in A then consider r1 being set such that A26: r1 in dom a9 and A27: r = a9 . r1 by FUNCT_1:def_3; AX . r1 in rng AX by A24, A26, FUNCT_1:def_3; then A28: the Sorts of M . (AX . r1) in rng the Sorts of M by A15, FUNCT_1:def_3; r in ( the Sorts of M * AX) . r1 by A23, A26, A27; then r in the Sorts of M . (AX . r1) by A24, A26, FUNCT_1:13; then r in union (rng the Sorts of M) by A28, TARSKI:def_4; then r in union (bool A) by A25; hence r in A by ZFMISC_1:81; ::_thesis: verum end; hence a in PFuncs (NAT,A) by A23, PARTFUN1:def_3; ::_thesis: verum end; then A29: dom Cm c= PFuncs (NAT,A) by XBOOLE_1:1; x1 in dom SR by A18, A19, PARTFUN1:def_2; then A30: SR . x1 = the Sorts of M . ( the ResultSort of S . x1) by FUNCT_1:12; the ResultSort of S . x1 in the carrier of S by A19, FUNCT_2:5; then SR . x1 in rng the Sorts of M by A15, A30, FUNCT_1:def_3; then rng Cm c= A by A16, XBOOLE_1:1; hence x in PFuncs ((PFuncs (NAT,A)),A) by A20, A29, PARTFUN1:def_3; ::_thesis: verum end; then ( SM9 in Funcs ( the carrier of S,(bool A)) & the Charact of M in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A18, FUNCT_2:8, FUNCT_2:def_2; then y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] by A17, ZFMISC_1:87; hence x in X by A6, A13, A17; ::_thesis: verum end; end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being set holds ( x in b2 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being set holds ( x in A2 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) implies A1 = A2 ) assume A31: for x being set holds ( x in A1 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ; ::_thesis: ( ex x being set st ( ( x in A2 implies ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) implies ( ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) & not x in A2 ) ) or A1 = A2 ) assume A32: for x being set holds ( x in A2 iff ex N being strict feasible MSAlgebra over S st ( x = N & ( for C being Component of the Sorts of N holds C c= A ) ) ) ; ::_thesis: A1 = A2 A33: A2 c= A1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A2 or a in A1 ) assume a in A2 ; ::_thesis: a in A1 then ex M being strict feasible MSAlgebra over S st ( a = M & ( for C being Component of the Sorts of M holds C c= A ) ) by A32; hence a in A1 by A31; ::_thesis: verum end; A1 c= A2 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in A2 ) assume a in A1 ; ::_thesis: a in A2 then ex M being strict feasible MSAlgebra over S st ( a = M & ( for C being Component of the Sorts of M holds C c= A ) ) by A31; hence a in A2 by A32; ::_thesis: verum end; hence A1 = A2 by A33, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def2 defines MSAlg_set MSINST_1:def_2_:_ for S being non empty non void ManySortedSign for A being non empty set for b3 being set holds ( b3 = MSAlg_set (S,A) iff for x being set holds ( x in b3 iff ex M being strict feasible MSAlgebra over S st ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ); registration let S be non empty non void ManySortedSign ; let A be non empty set ; cluster MSAlg_set (S,A) -> non empty ; coherence not MSAlg_set (S,A) is empty proof set a = the Element of A; reconsider f = the carrier of S --> { the Element of A} as ManySortedSet of the carrier of S ; set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S; set Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #); reconsider Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) as non-empty MSAlgebra over S by MSUALG_1:def_3; reconsider Ex = Ex as strict feasible MSAlgebra over S ; for C being Component of the Sorts of Ex holds C c= A proof let C be Component of the Sorts of Ex; ::_thesis: C c= A ex i being set st ( i in the carrier of S & C = the Sorts of Ex . i ) by PBOOLE:138; then C = { the Element of A} by FUNCOP_1:7; hence C c= A by ZFMISC_1:31; ::_thesis: verum end; hence not MSAlg_set (S,A) is empty by Def2; ::_thesis: verum end; end; begin theorem :: MSINST_1:2 for A being non empty set for S being non empty non void ManySortedSign for x being MSAlgebra over S st x in MSAlg_set (S,A) holds ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) proof let A be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for x being MSAlgebra over S st x in MSAlg_set (S,A) holds ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) let S be non empty non void ManySortedSign ; ::_thesis: for x being MSAlgebra over S st x in MSAlg_set (S,A) holds ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) let x be MSAlgebra over S; ::_thesis: ( x in MSAlg_set (S,A) implies ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) ) assume x in MSAlg_set (S,A) ; ::_thesis: ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) then consider M being strict feasible MSAlgebra over S such that A1: x = M and A2: for C being Component of the Sorts of M holds C c= A by Def2; A3: dom the Sorts of M = the carrier of S by PARTFUN1:def_2; then reconsider SM = the Sorts of M as Function of the carrier of S,(rng the Sorts of M) by FUNCT_2:1; A4: rng the Sorts of M c= bool A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of M or x in bool A ) assume x in rng the Sorts of M ; ::_thesis: x in bool A then reconsider x9 = x as Component of the Sorts of M ; x9 c= A by A2; hence x in bool A ; ::_thesis: verum end; then reconsider SM9 = SM as Function of the carrier of S,(bool A) by FUNCT_2:6; A5: dom the Charact of M = the carrier' of S by PARTFUN1:def_2; A6: rng the Charact of M c= PFuncs ((PFuncs (NAT,A)),A) proof reconsider SA = ( the Sorts of M #) * the Arity of S, SR = the Sorts of M * the ResultSort of S as ManySortedSet of the carrier' of S ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Charact of M or x in PFuncs ((PFuncs (NAT,A)),A) ) reconsider CM = the Charact of M as ManySortedFunction of SA,SR ; assume x in rng the Charact of M ; ::_thesis: x in PFuncs ((PFuncs (NAT,A)),A) then consider x1 being set such that A7: x1 in dom the Charact of M and A8: x = the Charact of M . x1 by FUNCT_1:def_3; reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A7, PBOOLE:def_15; A9: x1 in dom SA by A5, A7, PARTFUN1:def_2; SA . x1 c= PFuncs (NAT,A) proof reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A7, FUNCT_2:5; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SA . x1 or a in PFuncs (NAT,A) ) assume a in SA . x1 ; ::_thesis: a in PFuncs (NAT,A) then A10: a in ( the Sorts of M #) . ( the Arity of S . x1) by A9, FUNCT_1:12; ( the Sorts of M #) . AX = product ( the Sorts of M * AX) by FINSEQ_2:def_5; then A11: ex g being Function st ( a = g & dom g = dom ( the Sorts of M * AX) & ( for x2 being set st x2 in dom ( the Sorts of M * AX) holds g . x2 in ( the Sorts of M * AX) . x2 ) ) by A10, CARD_3:def_5; then reconsider a9 = a as Function ; rng AX c= dom the Sorts of M by A3; then A12: dom a9 = dom AX by A11, RELAT_1:27; rng a9 c= A proof rng the Sorts of M c= bool A proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng the Sorts of M or w in bool A ) assume w in rng the Sorts of M ; ::_thesis: w in bool A then reconsider w9 = w as Component of the Sorts of M ; w9 c= A by A2; hence w in bool A ; ::_thesis: verum end; then A13: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:77; let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng a9 or r in A ) assume r in rng a9 ; ::_thesis: r in A then consider r1 being set such that A14: r1 in dom a9 and A15: r = a9 . r1 by FUNCT_1:def_3; AX . r1 in rng AX by A12, A14, FUNCT_1:def_3; then A16: the Sorts of M . (AX . r1) in rng the Sorts of M by A3, FUNCT_1:def_3; r in ( the Sorts of M * AX) . r1 by A11, A14, A15; then r in the Sorts of M . (AX . r1) by A12, A14, FUNCT_1:13; then r in union (rng the Sorts of M) by A16, TARSKI:def_4; then r in union (bool A) by A13; hence r in A by ZFMISC_1:81; ::_thesis: verum end; hence a in PFuncs (NAT,A) by A11, PARTFUN1:def_3; ::_thesis: verum end; then A17: dom Cm c= PFuncs (NAT,A) by XBOOLE_1:1; x1 in dom SR by A5, A7, PARTFUN1:def_2; then A18: SR . x1 = the Sorts of M . ( the ResultSort of S . x1) by FUNCT_1:12; the ResultSort of S . x1 in the carrier of S by A7, FUNCT_2:5; then SR . x1 in rng the Sorts of M by A3, A18, FUNCT_1:def_3; then rng Cm c= A by A4, XBOOLE_1:1; hence x in PFuncs ((PFuncs (NAT,A)),A) by A8, A17, PARTFUN1:def_3; ::_thesis: verum end; SM9 in Funcs ( the carrier of S,(bool A)) by FUNCT_2:8; hence ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A1, A5, A6, FUNCT_2:def_2; ::_thesis: verum end; theorem Th3: :: MSINST_1:3 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds Args (o,U2) <> {} proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds Args (o,U2) <> {} let o be OperSymbol of S; ::_thesis: for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds Args (o,U2) <> {} let U1, U2 be MSAlgebra over S; ::_thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} implies Args (o,U2) <> {} ) assume that A1: the Sorts of U1 is_transformable_to the Sorts of U2 and A2: Args (o,U1) <> {} ; ::_thesis: Args (o,U2) <> {} A3: (( the Sorts of U1 #) * the Arity of S) . o <> {} by A2, MSUALG_1:def_4; dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom the Sorts of U1 ; then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; A5: dom ( the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:25; A6: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then (( the Sorts of U1 #) * the Arity of S) . o = ( the Sorts of U1 #) . ( the Arity of S . o) by FUNCT_1:13 .= ( the Sorts of U1 #) . (the_arity_of o) by MSUALG_1:def_1 ; then product ( the Sorts of U1 * (the_arity_of o)) <> {} by A3, FINSEQ_2:def_5; then A7: not {} in rng ( the Sorts of U1 * (the_arity_of o)) by CARD_3:26; now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_U2_*_(the_arity_of_o))_holds_ (_the_Sorts_of_U2_*_(the_arity_of_o))_._x_<>_{} let x be set ; ::_thesis: ( x in dom ( the Sorts of U2 * (the_arity_of o)) implies ( the Sorts of U2 * (the_arity_of o)) . x <> {} ) assume A8: x in dom ( the Sorts of U2 * (the_arity_of o)) ; ::_thesis: ( the Sorts of U2 * (the_arity_of o)) . x <> {} then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def_3; then A9: ( the Sorts of U1 . ((the_arity_of o) . x) <> {} implies the Sorts of U2 . ((the_arity_of o) . x) <> {} ) by A1, PZFMISC1:def_3; ( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A5, A8, FUNCT_1:13; hence ( the Sorts of U2 * (the_arity_of o)) . x <> {} by A7, A4, A5, A8, A9, FUNCT_1:13, FUNCT_1:def_3; ::_thesis: verum end; then not {} in rng ( the Sorts of U2 * (the_arity_of o)) by FUNCT_1:def_3; then product ( the Sorts of U2 * (the_arity_of o)) <> {} by CARD_3:26; then ( the Sorts of U2 #) . (the_arity_of o) <> {} by FINSEQ_2:def_5; then ( the Sorts of U2 #) . ( the Arity of S . o) <> {} by MSUALG_1:def_1; then (( the Sorts of U2 #) * the Arity of S) . o <> {} by A6, FUNCT_1:13; hence Args (o,U2) <> {} by MSUALG_1:def_4; ::_thesis: verum end; theorem Th4: :: MSINST_1:4 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1, U2, U3 being feasible MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1, U2, U3 being feasible MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) let o be OperSymbol of S; ::_thesis: for U1, U2, U3 being feasible MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) let U1, U2, U3 be feasible MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) let G be ManySortedFunction of U2,U3; ::_thesis: for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) let x be Element of Args (o,U1); ::_thesis: ( Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 implies ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) ) assume that A1: Args (o,U1) <> {} and A2: the Sorts of U1 is_transformable_to the Sorts of U2 and A3: the Sorts of U2 is_transformable_to the Sorts of U3 ; ::_thesis: ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF # x = G # (F # x) ) x in Args (o,U1) by A1; then x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then A4: ex g being Function st ( x = g & dom g = dom ( the Sorts of U1 * (the_arity_of o)) & ( for x being set st x in dom ( the Sorts of U1 * (the_arity_of o)) holds g . x in ( the Sorts of U1 * (the_arity_of o)) . x ) ) by CARD_3:def_5; then reconsider x9 = x as Function ; reconsider Fr = (Frege (F * (the_arity_of o))) . x9 as Function ; dom F = the carrier of S by PARTFUN1:def_2; then A5: rng (the_arity_of o) c= dom F ; then A6: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; A7: dom (doms (F * (the_arity_of o))) = dom (F * (the_arity_of o)) by FUNCT_6:59; then A8: dom x9 = dom (doms (F * (the_arity_of o))) by A1, A6, MSUALG_3:6; then reconsider x99 = x9 as ManySortedSet of dom (the_arity_of o) by A6, A7, PARTFUN1:def_2, RELAT_1:def_18; dom G = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom G ; then A9: dom (G * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; then reconsider Ga = G * (the_arity_of o), Fa = F * (the_arity_of o) as ManySortedFunction of dom (the_arity_of o) by A6, PARTFUN1:def_2, RELAT_1:def_18; A10: Args (o,U2) <> {} by A1, A2, Th3; dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2; then A11: rng (the_arity_of o) c= dom the Sorts of U1 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_(F_*_(the_arity_of_o)))_holds_ x9_._x_in_(doms_(F_*_(the_arity_of_o)))_._x let x be set ; ::_thesis: ( x in dom (doms (F * (the_arity_of o))) implies x9 . x in (doms (F * (the_arity_of o))) . x ) set ds = (the_arity_of o) . x; assume x in dom (doms (F * (the_arity_of o))) ; ::_thesis: x9 . x in (doms (F * (the_arity_of o))) . x then A12: x in dom (F * (the_arity_of o)) by FUNCT_6:59; then A13: (doms (F * (the_arity_of o))) . x = dom ((F * (the_arity_of o)) . x) by FUNCT_6:22; A14: x in dom (the_arity_of o) by A5, A12, RELAT_1:27; then A15: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider Ff = F . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U2 . ((the_arity_of o) . x)) by PBOOLE:def_15; x in dom ( the Sorts of U1 * (the_arity_of o)) by A11, A14, RELAT_1:27; then A16: x9 . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6; A17: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff proof percases ( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} ) ; suppose the Sorts of U2 . ((the_arity_of o) . x) <> {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff by FUNCT_2:def_1; ::_thesis: verum end; suppose the Sorts of U2 . ((the_arity_of o) . x) = {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff then the Sorts of U1 . ((the_arity_of o) . x) = {} by A2, A15, PZFMISC1:def_3; hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; ::_thesis: verum end; end; end; (F * (the_arity_of o)) . x = F . ((the_arity_of o) . x) by A14, FUNCT_1:13; hence x9 . x in (doms (F * (the_arity_of o))) . x by A13, A14, A16, A17, FUNCT_1:13; ::_thesis: verum end; then A18: x9 in product (doms (F * (the_arity_of o))) by A8, CARD_3:9; then A19: Fr = (F * (the_arity_of o)) .. x9 by PRALG_2:def_2; A20: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_(G_*_(the_arity_of_o)))_holds_ Fr_._x_in_(doms_(G_*_(the_arity_of_o)))_._x let x be set ; ::_thesis: ( x in dom (doms (G * (the_arity_of o))) implies Fr . x in (doms (G * (the_arity_of o))) . x ) set ds = (the_arity_of o) . x; assume A21: x in dom (doms (G * (the_arity_of o))) ; ::_thesis: Fr . x in (doms (G * (the_arity_of o))) . x then A22: x in dom (G * (the_arity_of o)) by FUNCT_6:59; x in dom (F * (the_arity_of o)) by A9, A6, A21, FUNCT_6:59; then A23: Fr . x = ((F * (the_arity_of o)) . x) . (x9 . x) by A19, PRALG_1:def_17; A24: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A11, RELAT_1:27; A25: x in dom (the_arity_of o) by A9, A21, FUNCT_6:59; then A26: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider Ff = F . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U2 . ((the_arity_of o) . x)) by PBOOLE:def_15; A27: (F * (the_arity_of o)) . x = Ff by A6, A25, FUNCT_1:12; reconsider Gds = G . ((the_arity_of o) . x) as Function of ( the Sorts of U2 . ((the_arity_of o) . x)),( the Sorts of U3 . ((the_arity_of o) . x)) by A26, PBOOLE:def_15; A28: dom Gds = the Sorts of U2 . ((the_arity_of o) . x) proof percases ( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} ) ; suppose the Sorts of U3 . ((the_arity_of o) . x) <> {} ; ::_thesis: dom Gds = the Sorts of U2 . ((the_arity_of o) . x) hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) by FUNCT_2:def_1; ::_thesis: verum end; suppose the Sorts of U3 . ((the_arity_of o) . x) = {} ; ::_thesis: dom Gds = the Sorts of U2 . ((the_arity_of o) . x) then the Sorts of U2 . ((the_arity_of o) . x) = {} by A3, A26, PZFMISC1:def_3; hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) ; ::_thesis: verum end; end; end; A29: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff proof percases ( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} ) ; suppose the Sorts of U2 . ((the_arity_of o) . x) <> {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff by FUNCT_2:def_1; ::_thesis: verum end; suppose the Sorts of U2 . ((the_arity_of o) . x) = {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff then the Sorts of U1 . ((the_arity_of o) . x) = {} by A2, A26, PZFMISC1:def_3; hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; ::_thesis: verum end; end; end; ( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A25, FUNCT_1:13; then x9 . x in dom Ff by A1, A25, A24, A29, MSUALG_3:6; then A30: ((F * (the_arity_of o)) . x) . (x9 . x) in rng Ff by A27, FUNCT_1:def_3; (G * (the_arity_of o)) . x = G . ((the_arity_of o) . x) by A25, FUNCT_1:13; then Fr . x in dom ((G * (the_arity_of o)) . x) by A28, A30, A23; hence Fr . x in (doms (G * (the_arity_of o))) . x by A22, FUNCT_6:22; ::_thesis: verum end; reconsider GF = G ** F as ManySortedFunction of U1,U3 by A2, ALTCAT_2:4; dom GF = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom GF ; then A31: dom (GF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; A32: x99 in doms Fa proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in dom (the_arity_of o) or x99 . i in (doms Fa) . i ) set ai = (the_arity_of o) . i; assume A33: i in dom (the_arity_of o) ; ::_thesis: x99 . i in (doms Fa) . i then A34: (the_arity_of o) . i in rng (the_arity_of o) by FUNCT_1:def_3; Fa . i = F . ((the_arity_of o) . i) by A33, FUNCT_1:13; then reconsider Ew = Fa . i as Function of ( the Sorts of U1 . ((the_arity_of o) . i)),( the Sorts of U2 . ((the_arity_of o) . i)) by A34, PBOOLE:def_15; A35: dom Ew = the Sorts of U1 . ((the_arity_of o) . i) proof percases ( the Sorts of U2 . ((the_arity_of o) . i) = {} or the Sorts of U2 . ((the_arity_of o) . i) <> {} ) ; suppose the Sorts of U2 . ((the_arity_of o) . i) = {} ; ::_thesis: dom Ew = the Sorts of U1 . ((the_arity_of o) . i) then the Sorts of U1 . ((the_arity_of o) . i) = {} by A2, A34, PZFMISC1:def_3; hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) ; ::_thesis: verum end; suppose the Sorts of U2 . ((the_arity_of o) . i) <> {} ; ::_thesis: dom Ew = the Sorts of U1 . ((the_arity_of o) . i) hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) by FUNCT_2:def_1; ::_thesis: verum end; end; end; i in dom ( the Sorts of U1 * (the_arity_of o)) by A33, PRALG_2:3; then x99 . i in ( the Sorts of U1 * (the_arity_of o)) . i by A4; then x99 . i in dom (Fa . i) by A33, A35, FUNCT_1:13; hence x99 . i in (doms Fa) . i by A33, MSSUBFAM:14; ::_thesis: verum end; take GF ; ::_thesis: ( GF = G ** F & GF # x = G # (F # x) ) thus GF = G ** F ; ::_thesis: GF # x = G # (F # x) A36: (G * (the_arity_of o)) ** (F * (the_arity_of o)) = GF * (the_arity_of o) by FUNCTOR0:12; A37: the Sorts of U1 is_transformable_to the Sorts of U3 by A2, A3, AUTALG_1:10; A38: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_(GF_*_(the_arity_of_o)))_holds_ x9_._x_in_(doms_(GF_*_(the_arity_of_o)))_._x let x be set ; ::_thesis: ( x in dom (doms (GF * (the_arity_of o))) implies x9 . x in (doms (GF * (the_arity_of o))) . x ) set ds = (the_arity_of o) . x; assume A39: x in dom (doms (GF * (the_arity_of o))) ; ::_thesis: x9 . x in (doms (GF * (the_arity_of o))) . x then A40: x in dom (the_arity_of o) by A31, FUNCT_6:59; then A41: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider Gf = GF . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U3 . ((the_arity_of o) . x)) by PBOOLE:def_15; x in dom (GF * (the_arity_of o)) by A39, FUNCT_6:59; then A42: (doms (GF * (the_arity_of o))) . x = dom ((GF * (the_arity_of o)) . x) by FUNCT_6:22; A43: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf proof percases ( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} ) ; suppose the Sorts of U3 . ((the_arity_of o) . x) <> {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf by FUNCT_2:def_1; ::_thesis: verum end; suppose the Sorts of U3 . ((the_arity_of o) . x) = {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf then the Sorts of U1 . ((the_arity_of o) . x) = {} by A37, A41, PZFMISC1:def_3; hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf ; ::_thesis: verum end; end; end; x in dom ( the Sorts of U1 * (the_arity_of o)) by A11, A40, RELAT_1:27; then x9 . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6; then x9 . x in dom (GF . ((the_arity_of o) . x)) by A40, A43, FUNCT_1:13; hence x9 . x in (doms (GF * (the_arity_of o))) . x by A42, A40, FUNCT_1:13; ::_thesis: verum end; dom (doms (GF * (the_arity_of o))) = dom (GF * (the_arity_of o)) by FUNCT_6:59; then dom x9 = dom (doms (GF * (the_arity_of o))) by A1, A31, MSUALG_3:6; then A44: x9 in product (doms (GF * (the_arity_of o))) by A38, CARD_3:9; dom Fr = dom (G * (the_arity_of o)) by A9, A6, A19, PRALG_1:def_17; then dom Fr = dom (doms (G * (the_arity_of o))) by FUNCT_6:59; then Fr in product (doms (G * (the_arity_of o))) by A20, CARD_3:9; then A45: (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) = (G * (the_arity_of o)) .. ((Frege (F * (the_arity_of o))) . x) by PRALG_2:def_2 .= Ga .. (Fa .. x99) by A18, PRALG_2:def_2 .= (Ga ** Fa) .. x99 by A32, CLOSURE1:4 ; A46: Args (o,U3) <> {} by A1, A2, A3, Th3, AUTALG_1:10; then GF # x = (Frege (GF * (the_arity_of o))) . x by A1, MSUALG_3:def_5 .= (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) by A44, A45, A36, PRALG_2:def_2 .= (Frege (G * (the_arity_of o))) . (F # x) by A1, A10, MSUALG_3:def_5 ; hence GF # x = G # (F # x) by A10, A46, MSUALG_3:def_5; ::_thesis: verum end; theorem Th5: :: MSINST_1:5 for S being non empty non void ManySortedSign for U1, U2, U3 being feasible MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF is_homomorphism U1,U3 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being feasible MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF is_homomorphism U1,U3 ) let U1, U2, U3 be feasible MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF is_homomorphism U1,U3 ) let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF is_homomorphism U1,U3 ) let G be ManySortedFunction of U2,U3; ::_thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 implies ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF is_homomorphism U1,U3 ) ) assume that A1: the Sorts of U1 is_transformable_to the Sorts of U2 and A2: the Sorts of U2 is_transformable_to the Sorts of U3 and A3: F is_homomorphism U1,U2 and A4: G is_homomorphism U2,U3 ; ::_thesis: ex GF being ManySortedFunction of U1,U3 st ( GF = G ** F & GF is_homomorphism U1,U3 ) reconsider GF = G ** F as ManySortedFunction of U1,U3 by A1, ALTCAT_2:4; take GF ; ::_thesis: ( GF = G ** F & GF is_homomorphism U1,U3 ) thus GF = G ** F ; ::_thesis: GF is_homomorphism U1,U3 thus GF is_homomorphism U1,U3 ::_thesis: verum proof let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) = {} or for b1 being Element of Args (o,U1) holds (GF . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,U3)) . (GF # b1) ) assume A5: Args (o,U1) <> {} ; ::_thesis: for b1 being Element of Args (o,U1) holds (GF . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,U3)) . (GF # b1) let x be Element of Args (o,U1); ::_thesis: (GF . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x) A6: ex gf being ManySortedFunction of U1,U3 st ( gf = G ** F & gf # x = G # (F # x) ) by A1, A2, A5, Th4; set r = the_result_sort_of o; ( (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) & Args (o,U2) <> {} ) by A1, A3, A5, Th3, MSUALG_3:def_7; then A7: (G . (the_result_sort_of o)) . ((F . (the_result_sort_of o)) . ((Den (o,U1)) . x)) = (Den (o,U3)) . (G # (F # x)) by A4, MSUALG_3:def_7; A8: the Sorts of U1 is_transformable_to the Sorts of U3 by A1, A2, AUTALG_1:10; A9: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) proof percases ( the Sorts of U1 . (the_result_sort_of o) <> {} or the Sorts of U1 . (the_result_sort_of o) = {} ) ; suppose the Sorts of U1 . (the_result_sort_of o) <> {} ; ::_thesis: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) then the Sorts of U3 . (the_result_sort_of o) <> {} by A8, PZFMISC1:def_3; hence dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def_1; ::_thesis: verum end; suppose the Sorts of U1 . (the_result_sort_of o) = {} ; ::_thesis: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) hence dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) ; ::_thesis: verum end; end; end; o in the carrier' of S ; then A10: o in dom the ResultSort of S by FUNCT_2:def_1; rng the ResultSort of S c= the carrier of S ; then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def_2; then ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def_5, RELAT_1:27; then A11: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A10, FUNCT_1:12 .= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ; then ( GF . (the_result_sort_of o) = (G . (the_result_sort_of o)) * (F . (the_result_sort_of o)) & the Sorts of U1 . (the_result_sort_of o) <> {} ) by A5, MSUALG_3:2, MSUALG_6:def_1; hence (GF . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x) by A5, A7, A9, A11, A6, FUNCT_1:12, FUNCT_2:5; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let A be non empty set ; let i, j be set ; assume that A1: i in MSAlg_set (S,A) and A2: j in MSAlg_set (S,A) ; func MSAlg_morph (S,A,i,j) -> set means :Def3: :: MSINST_1:def 3 for x being set holds ( x in it iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) proof consider M being strict feasible MSAlgebra over S such that A3: i = M and A4: for C being Component of the Sorts of M holds C c= A by A1, Def2; consider N being strict feasible MSAlgebra over S such that A5: j = N and A6: for C being Component of the Sorts of N holds C c= A by A2, Def2; defpred S1[ set ] means ( the Sorts of M is_transformable_to the Sorts of N & ex f being ManySortedFunction of M,N st ( $1 = f & f is_homomorphism M,N ) ); consider X being set such that A7: for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) let x be set ; ::_thesis: ( x in X iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) hereby ::_thesis: ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) implies x in X ) assume A8: x in X ; ::_thesis: ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) then consider f being ManySortedFunction of M,N such that A9: x = f and A10: f is_homomorphism M,N by A7; take M = M; ::_thesis: ex N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) take N = N; ::_thesis: ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) reconsider f = f as ManySortedFunction of M,N ; take f = f; ::_thesis: ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) thus ( M = i & N = j & f = x ) by A3, A5, A9; ::_thesis: ( the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) thus the Sorts of M is_transformable_to the Sorts of N by A8, A7; ::_thesis: f is_homomorphism M,N thus f is_homomorphism M,N by A10; ::_thesis: verum end; given M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that A11: ( M1 = i & N1 = j & f = x & the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) ; ::_thesis: x in X reconsider F = f as ManySortedFunction of M,N by A11, A3, A5; A12: dom F = the carrier of S by PARTFUN1:def_2; rng F c= PFuncs ((union (bool A)),(union (bool A))) proof A13: rng the Sorts of M c= bool A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of M or x in bool A ) assume x in rng the Sorts of M ; ::_thesis: x in bool A then reconsider x9 = x as Component of the Sorts of M ; x9 c= A by A4; hence x in bool A ; ::_thesis: verum end; let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng F or w in PFuncs ((union (bool A)),(union (bool A))) ) assume w in rng F ; ::_thesis: w in PFuncs ((union (bool A)),(union (bool A))) then consider w1 being set such that A14: w1 in dom F and A15: w = F . w1 by FUNCT_1:def_3; reconsider w9 = w as Function of ( the Sorts of M . w1),( the Sorts of N . w1) by A14, A15, PBOOLE:def_15; A16: dom the Sorts of M = the carrier of S by PARTFUN1:def_2; A17: dom w9 c= union (bool A) proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in dom w9 or s in union (bool A) ) assume A18: s in dom w9 ; ::_thesis: s in union (bool A) the Sorts of M . w1 in rng the Sorts of M by A14, A16, FUNCT_1:def_3; hence s in union (bool A) by A13, A18, TARSKI:def_4; ::_thesis: verum end; A19: rng the Sorts of N c= bool A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of N or x in bool A ) assume x in rng the Sorts of N ; ::_thesis: x in bool A then reconsider x9 = x as Component of the Sorts of N ; x9 c= A by A6; hence x in bool A ; ::_thesis: verum end; A20: dom the Sorts of N = the carrier of S by PARTFUN1:def_2; rng w9 c= union (bool A) proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng w9 or r in union (bool A) ) assume A21: r in rng w9 ; ::_thesis: r in union (bool A) the Sorts of N . w1 in rng the Sorts of N by A14, A20, FUNCT_1:def_3; hence r in union (bool A) by A19, A21, TARSKI:def_4; ::_thesis: verum end; hence w in PFuncs ((union (bool A)),(union (bool A))) by A17, PARTFUN1:def_3; ::_thesis: verum end; then F in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) by A12, FUNCT_2:def_2; hence x in X by A7, A11, A3, A5; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds ( x in b2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds ( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) implies A1 = A2 ) assume A22: for x being set holds ( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; ::_thesis: ( ex x being set st ( ( x in A2 implies ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) implies ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) & not x in A2 ) ) or A1 = A2 ) assume A23: for x being set holds ( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; ::_thesis: A1 = A2 A24: A2 c= A1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A2 or a in A1 ) assume a in A2 ; ::_thesis: a in A1 then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A23; hence a in A1 by A22; ::_thesis: verum end; A1 c= A2 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in A2 ) assume a in A1 ; ::_thesis: a in A2 then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A22; hence a in A2 by A23; ::_thesis: verum end; hence A1 = A2 by A24, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def3 defines MSAlg_morph MSINST_1:def_3_:_ for S being non empty non void ManySortedSign for A being non empty set for i, j being set st i in MSAlg_set (S,A) & j in MSAlg_set (S,A) holds for b5 being set holds ( b5 = MSAlg_morph (S,A,i,j) iff for x being set holds ( x in b5 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ); definition let S be non empty non void ManySortedSign ; let A be non empty set ; func MSAlgCat (S,A) -> non empty strict AltCatStr means :Def4: :: MSINST_1:def 4 ( the carrier of it = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of it . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of it for f, g being Function-yielding Function st f in the Arrows of it . (i,j) & g in the Arrows of it . (j,k) holds ( the Comp of it . (i,j,k)) . (g,f) = g ** f ) ); existence ex b1 being non empty strict AltCatStr st ( the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b1 for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds ( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) ) proof set c = MSAlg_set (S,A); deffunc H1( Element of MSAlg_set (S,A), Element of MSAlg_set (S,A)) -> set = MSAlg_morph (S,A,$1,$2); consider M being ManySortedSet of [:(MSAlg_set (S,A)),(MSAlg_set (S,A)):] such that A1: for i, j being Element of MSAlg_set (S,A) holds M . (i,j) = H1(i,j) from ALTCAT_1:sch_2(); defpred S1[ set , set , set ] means ex i, j, k being Element of MSAlg_set (S,A) st ( $3 = [i,j,k] & ( for f, g being Function-yielding Function st f in M . (i,j) & g in M . (j,k) & $2 = [g,f] holds $1 = g ** f ) ); A2: for ijk being set st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds for x being set st x in {|M,M|} . ijk holds ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) proof let ijk be set ; ::_thesis: ( ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] implies for x being set st x in {|M,M|} . ijk holds ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) ) assume ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] ; ::_thesis: for x being set st x in {|M,M|} . ijk holds ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) then consider x1, x2, x3 being set such that A3: ( x1 in MSAlg_set (S,A) & x2 in MSAlg_set (S,A) & x3 in MSAlg_set (S,A) ) and A4: ijk = [x1,x2,x3] by MCART_1:68; reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSAlg_set (S,A) by A3; let x be set ; ::_thesis: ( x in {|M,M|} . ijk implies ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) ) A5: ( {|M,M|} . (x1,x2,x3) = {|M,M|} . [x1,x2,x3] & {|M,M|} . (x1,x2,x3) = [:(M . (x2,x3)),(M . (x1,x2)):] ) by ALTCAT_1:def_4, MULTOP_1:def_1; A6: {|M|} . ijk = {|M|} . (x1,x2,x3) by A4, MULTOP_1:def_1; assume A7: x in {|M,M|} . ijk ; ::_thesis: ex y being set st ( y in {|M|} . ijk & S1[y,x,ijk] ) then x `1 in M . (x2,x3) by A4, A5, MCART_1:10; then x `1 in MSAlg_morph (S,A,x2,x3) by A1; then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that A8: M2 = x2 and A9: N2 = x3 and A10: g = x `1 and A11: ( the Sorts of M2 is_transformable_to the Sorts of N2 & g is_homomorphism M2,N2 ) by Def3; x `2 in M . (x1,x2) by A4, A7, A5, MCART_1:10; then x `2 in MSAlg_morph (S,A,x1,x2) by A1; then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that A12: M1 = x1 and A13: N1 = x2 and A14: f = x `2 and A15: ( the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) by Def3; take y = g ** f; ::_thesis: ( y in {|M|} . ijk & S1[y,x,ijk] ) reconsider f = f as ManySortedFunction of M1,M2 by A8, A13; ( the Sorts of M1 is_transformable_to the Sorts of N2 & ex fg being ManySortedFunction of M1,N2 st ( fg = g ** f & fg is_homomorphism M1,N2 ) ) by A8, A11, A13, A15, Th5, AUTALG_1:10; then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSAlg_morph (S,A,x1,x3) ) by A9, A12, Def3, ALTCAT_1:def_3; hence y in {|M|} . ijk by A1, A6; ::_thesis: S1[y,x,ijk] take x1 ; ::_thesis: ex j, k being Element of MSAlg_set (S,A) st ( ijk = [x1,j,k] & ( for f, g being Function-yielding Function st f in M . (x1,j) & g in M . (j,k) & x = [g,f] holds y = g ** f ) ) take x2 ; ::_thesis: ex k being Element of MSAlg_set (S,A) st ( ijk = [x1,x2,k] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,k) & x = [g,f] holds y = g ** f ) ) take x3 ; ::_thesis: ( ijk = [x1,x2,x3] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds y = g ** f ) ) thus ijk = [x1,x2,x3] by A4; ::_thesis: for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds y = g ** f let F, G be Function-yielding Function; ::_thesis: ( F in M . (x1,x2) & G in M . (x2,x3) & x = [G,F] implies y = G ** F ) assume that F in M . (x1,x2) and G in M . (x2,x3) and A16: x = [G,F] ; ::_thesis: y = G ** F x `1 = G by A16, MCART_1:7; hence y = G ** F by A10, A14, A16, MCART_1:7; ::_thesis: verum end; consider F being ManySortedFunction of {|M,M|},{|M|} such that A17: for ijk being set st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st ( f = F . ijk & ( for x being set st x in {|M,M|} . ijk holds S1[f . x,x,ijk] ) ) from MSSUBFAM:sch_1(A2); take EX = AltCatStr(# (MSAlg_set (S,A)),M,F #); ::_thesis: ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of EX for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) ) reconsider EX = EX as non empty AltCatStr ; for i, j, k being object of EX for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . (g,f) = g ** f proof let i, j, k be object of EX; ::_thesis: for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . (g,f) = g ** f let f, g be Function-yielding Function; ::_thesis: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) assume A18: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) ) ; ::_thesis: ( the Comp of EX . (i,j,k)) . (g,f) = g ** f set x = [g,f]; set ijk = [i,j,k]; [i,j,k] in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] by MCART_1:69; then consider ff being Function of ({|M,M|} . [i,j,k]),({|M|} . [i,j,k]) such that A19: ff = F . [i,j,k] and A20: for x being set st x in {|M,M|} . [i,j,k] holds S1[ff . x,x,[i,j,k]] by A17; A21: ff = the Comp of EX . (i,j,k) by A19, MULTOP_1:def_1; ( {|M,M|} . (i,j,k) = {|M,M|} . [i,j,k] & {|M,M|} . (i,j,k) = [:(M . (j,k)),(M . (i,j)):] ) by ALTCAT_1:def_4, MULTOP_1:def_1; then [g,f] in {|M,M|} . [i,j,k] by A18, ZFMISC_1:87; then consider I, J, K being Element of MSAlg_set (S,A) such that A22: [i,j,k] = [I,J,K] and A23: for f, g being Function-yielding Function st f in M . (I,J) & g in M . (J,K) & [g,f] = [g,f] holds ff . [g,f] = g ** f by A20; A24: K = k by A22, XTUPLE_0:3; ( I = i & J = j ) by A22, XTUPLE_0:3; hence ( the Comp of EX . (i,j,k)) . (g,f) = g ** f by A18, A23, A24, A21; ::_thesis: verum end; hence ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of EX for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds ( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b1 for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds ( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) & the carrier of b2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b2 for f, g being Function-yielding Function st f in the Arrows of b2 . (i,j) & g in the Arrows of b2 . (j,k) holds ( the Comp of b2 . (i,j,k)) . (g,f) = g ** f ) holds b1 = b2 proof reconsider c = MSAlg_set (S,A) as non empty set ; let A1, A2 be non empty strict AltCatStr ; ::_thesis: ( the carrier of A1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of A1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of A1 for f, g being Function-yielding Function st f in the Arrows of A1 . (i,j) & g in the Arrows of A1 . (j,k) holds ( the Comp of A1 . (i,j,k)) . (g,f) = g ** f ) & the carrier of A2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of A2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of A2 for f, g being Function-yielding Function st f in the Arrows of A2 . (i,j) & g in the Arrows of A2 . (j,k) holds ( the Comp of A2 . (i,j,k)) . (g,f) = g ** f ) implies A1 = A2 ) assume that A25: the carrier of A1 = MSAlg_set (S,A) and A26: for i, j being Element of MSAlg_set (S,A) holds the Arrows of A1 . (i,j) = MSAlg_morph (S,A,i,j) and A27: for i, j, k being object of A1 for f, g being Function-yielding Function st f in the Arrows of A1 . (i,j) & g in the Arrows of A1 . (j,k) holds ( the Comp of A1 . (i,j,k)) . (g,f) = g ** f and A28: the carrier of A2 = MSAlg_set (S,A) and A29: for i, j being Element of MSAlg_set (S,A) holds the Arrows of A2 . (i,j) = MSAlg_morph (S,A,i,j) and A30: for i, j, k being object of A2 for f, g being Function-yielding Function st f in the Arrows of A2 . (i,j) & g in the Arrows of A2 . (j,k) holds ( the Comp of A2 . (i,j,k)) . (g,f) = g ** f ; ::_thesis: A1 = A2 reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:c,c,c:] by A25, A28; reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of [:c,c:] by A25, A28; A31: now__::_thesis:_for_i,_j_being_Element_of_c_holds_AA1_._(i,j)_=_AA2_._(i,j) let i, j be Element of c; ::_thesis: AA1 . (i,j) = AA2 . (i,j) thus AA1 . (i,j) = MSAlg_morph (S,A,i,j) by A26 .= AA2 . (i,j) by A29 ; ::_thesis: verum end; then A32: AA1 = AA2 by ALTCAT_1:7; now__::_thesis:_for_i,_j,_k_being_set_st_i_in_c_&_j_in_c_&_k_in_c_holds_ CC1_._(i,j,k)_=_CC2_._(i,j,k) let i, j, k be set ; ::_thesis: ( i in c & j in c & k in c implies CC1 . (i,j,k) = CC2 . (i,j,k) ) set ijk = [i,j,k]; A33: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def_1; assume A34: ( i in c & j in c & k in c ) ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k) then reconsider i9 = i, j9 = j, k9 = k as Element of c ; reconsider I9 = i, J9 = j, K9 = k as object of A2 by A28, A34; reconsider I = i, J = j, K = k as object of A1 by A25, A34; A35: [i,j,k] in [:c,c,c:] by A34, MCART_1:69; A36: CC2 . (i,j,k) = CC2 . [i,j,k] by MULTOP_1:def_1; thus CC1 . (i,j,k) = CC2 . (i,j,k) ::_thesis: verum proof reconsider Cj = CC2 . [i,j,k] as Function of ({|AA2,AA2|} . [i,j,k]),({|AA2|} . [i,j,k]) by A28, A35, PBOOLE:def_15; reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A25, A35, PBOOLE:def_15; percases ( {|AA1|} . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} ) ; supposeA37: {|AA1|} . [i,j,k] <> {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k) A38: for x being set st x in {|AA1,AA1|} . [i,j,k] holds Ci . x = Cj . x proof let x be set ; ::_thesis: ( x in {|AA1,AA1|} . [i,j,k] implies Ci . x = Cj . x ) assume A39: x in {|AA1,AA1|} . [i,j,k] ; ::_thesis: Ci . x = Cj . x then x in {|AA1,AA1|} . (i,j,k) by MULTOP_1:def_1; then A40: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A34, ALTCAT_1:def_4; then A41: x `1 in AA1 . (j,k) by MCART_1:10; then x `1 in MSAlg_morph (S,A,j9,k9) by A26; then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that M2 = j9 and N2 = k9 and A42: g = x `1 and the Sorts of M2 is_transformable_to the Sorts of N2 and g is_homomorphism M2,N2 by Def3; x in {|AA2,AA2|} . (i,j,k) by A32, A39, MULTOP_1:def_1; then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A34, ALTCAT_1:def_4; then A43: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10; A44: x `2 in AA1 . (i,j) by A40, MCART_1:10; then x `2 in MSAlg_morph (S,A,i9,j9) by A26; then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that M1 = i9 and N1 = j9 and A45: f = x `2 and the Sorts of M1 is_transformable_to the Sorts of N1 and f is_homomorphism M1,N1 by Def3; A46: x = [g,f] by A40, A45, A42, MCART_1:21; then Ci . x = ( the Comp of A1 . (I,J,K)) . (g,f) by MULTOP_1:def_1 .= g ** f by A27, A41, A44, A45, A42 .= ( the Comp of A2 . (I9,J9,K9)) . (g,f) by A30, A43, A45, A42 .= Cj . x by A46, MULTOP_1:def_1 ; hence Ci . x = Cj . x ; ::_thesis: verum end; {|AA2|} . [i,j,k] <> {} by A31, A37, ALTCAT_1:7; then A47: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def_1; dom Ci = {|AA1,AA1|} . [i,j,k] by A37, FUNCT_2:def_1; hence CC1 . (i,j,k) = CC2 . (i,j,k) by A32, A33, A36, A47, A38, FUNCT_1:2; ::_thesis: verum end; suppose {|AA1|} . [i,j,k] = {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k) then ( Ci = {} & Cj = {} ) by A32; hence CC1 . (i,j,k) = CC2 . (i,j,k) by A33, MULTOP_1:def_1; ::_thesis: verum end; end; end; end; hence A1 = A2 by A25, A28, A32, ALTCAT_1:8; ::_thesis: verum end; end; :: deftheorem Def4 defines MSAlgCat MSINST_1:def_4_:_ for S being non empty non void ManySortedSign for A being non empty set for b3 being non empty strict AltCatStr holds ( b3 = MSAlgCat (S,A) iff ( the carrier of b3 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b3 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b3 for f, g being Function-yielding Function st f in the Arrows of b3 . (i,j) & g in the Arrows of b3 . (j,k) holds ( the Comp of b3 . (i,j,k)) . (g,f) = g ** f ) ) ); registration let S be non empty non void ManySortedSign ; let A be non empty set ; cluster MSAlgCat (S,A) -> non empty transitive strict associative with_units ; coherence ( MSAlgCat (S,A) is transitive & MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units ) proof set M = MSAlgCat (S,A); set G = MSAlgCat (S,A); set GM = the Arrows of (MSAlgCat (S,A)); set C = the Comp of (MSAlgCat (S,A)); thus MSAlgCat (S,A) is transitive ::_thesis: ( MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units ) proof let o1, o2, o3 be object of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} ) reconsider o19 = o1, o29 = o2, o39 = o3 as Element of MSAlg_set (S,A) by Def4; assume that A1: <^o1,o2^> <> {} and A2: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {} set t = the Element of MSAlg_morph (S,A,o19,o29); MSAlg_morph (S,A,o19,o29) <> {} by A1, Def4; then consider M, N being strict feasible MSAlgebra over S, f being ManySortedFunction of M,N such that A3: M = o19 and A4: N = o29 and f = the Element of MSAlg_morph (S,A,o19,o29) and A5: the Sorts of M is_transformable_to the Sorts of N and A6: f is_homomorphism M,N by Def3; set s = the Element of MSAlg_morph (S,A,o29,o39); MSAlg_morph (S,A,o29,o39) <> {} by A2, Def4; then consider M1, N1 being strict feasible MSAlgebra over S, g being ManySortedFunction of M1,N1 such that A7: M1 = o29 and A8: N1 = o39 and g = the Element of MSAlg_morph (S,A,o29,o39) and A9: the Sorts of M1 is_transformable_to the Sorts of N1 and A10: g is_homomorphism M1,N1 by Def3; reconsider g9 = g as ManySortedFunction of N,N1 by A4, A7; consider GF being ManySortedFunction of M,N1 such that GF = g9 ** f and A11: GF is_homomorphism M,N1 by A4, A5, A6, A7, A9, A10, Th5; the Sorts of M is_transformable_to the Sorts of N1 by A4, A5, A7, A9, AUTALG_1:10; then GF in MSAlg_morph (S,A,o19,o39) by A3, A8, A11, Def3; hence not <^o1,o3^> = {} by Def4; ::_thesis: verum end; thus the Comp of (MSAlgCat (S,A)) is associative :: according to ALTCAT_1:def_15 ::_thesis: MSAlgCat (S,A) is with_units proof let i, j, k, l be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds ( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or not b2 in the Arrows of (MSAlgCat (S,A)) . (j,k) or not b3 in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (b3,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (b3,b2)),b1) ) let f, g, h be set ; ::_thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or not g in the Arrows of (MSAlgCat (S,A)) . (j,k) or not h in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) ) reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of MSAlg_set (S,A) by Def4; assume that A12: f in the Arrows of (MSAlgCat (S,A)) . (i,j) and A13: g in the Arrows of (MSAlgCat (S,A)) . (j,k) and A14: h in the Arrows of (MSAlgCat (S,A)) . (k,l) ; ::_thesis: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) g in MSAlg_morph (S,A,j9,k9) by A13, Def4; then consider M2, N2 being strict feasible MSAlgebra over S, G being ManySortedFunction of M2,N2 such that A15: M2 = j9 and A16: N2 = k9 and A17: g = G and A18: the Sorts of M2 is_transformable_to the Sorts of N2 and A19: G is_homomorphism M2,N2 by Def3; h in MSAlg_morph (S,A,k9,l9) by A14, Def4; then consider M3, N3 being strict feasible MSAlgebra over S, H being ManySortedFunction of M3,N3 such that A20: M3 = k9 and A21: N3 = l9 and A22: h = H and A23: the Sorts of M3 is_transformable_to the Sorts of N3 and A24: H is_homomorphism M3,N3 by Def3; reconsider G9 = G as ManySortedFunction of M2,M3 by A16, A20; consider HG being ManySortedFunction of M2,N3 such that A25: HG = H ** G9 and A26: HG is_homomorphism M2,N3 by A16, A18, A19, A20, A23, A24, Th5; A27: ( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (H,G) = H ** G9 by A13, A14, A17, A22, Def4; f in MSAlg_morph (S,A,i9,j9) by A12, Def4; then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that A28: M1 = i9 and A29: N1 = j9 and A30: f = F and A31: the Sorts of M1 is_transformable_to the Sorts of N1 and A32: F is_homomorphism M1,N1 by Def3; A33: ( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f) = G ** F by A12, A13, A30, A17, Def4; consider GF being ManySortedFunction of M1,M3 such that A34: GF = G9 ** F and A35: GF is_homomorphism M1,M3 by A29, A31, A32, A15, A16, A18, A19, A20, Th5; the Sorts of M1 is_transformable_to the Sorts of M3 by A29, A31, A15, A16, A18, A20, AUTALG_1:10; then G9 ** F in MSAlg_morph (S,A,i9,k9) by A28, A20, A34, A35, Def3; then GF in the Arrows of (MSAlgCat (S,A)) . (i,k) by A34, Def4; then A36: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (H,GF) = H ** GF by A14, A22, Def4; the Sorts of M2 is_transformable_to the Sorts of N3 by A16, A18, A20, A23, AUTALG_1:10; then HG in MSAlg_morph (S,A,j9,l9) by A15, A21, A26, Def3; then A37: H ** G9 in the Arrows of (MSAlgCat (S,A)) . (j,l) by A25, Def4; (H ** G9) ** F = H ** (G9 ** F) by PBOOLE:140; hence ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) by A12, A30, A17, A22, A33, A34, A36, A27, A37, Def4; ::_thesis: verum end; thus the Comp of (MSAlgCat (S,A)) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (MSAlgCat (S,A)) is with_right_units proof let j be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st ( b1 in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b2 being Element of the carrier of (MSAlgCat (S,A)) for b3 being set holds ( not b3 in the Arrows of (MSAlgCat (S,A)) . (b2,j) or ( the Comp of (MSAlgCat (S,A)) . (b2,j,j)) . (b1,b3) = b3 ) ) ) reconsider j9 = j as Element of MSAlg_set (S,A) by Def4; consider MS being strict feasible MSAlgebra over S such that A38: MS = j9 and for C being Component of the Sorts of MS holds C c= A by Def2; reconsider e = id the Sorts of MS as ManySortedFunction of MS,MS ; take e ; ::_thesis: ( e in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b1 being Element of the carrier of (MSAlgCat (S,A)) for b2 being set holds ( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 ) ) ) ( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (j,j) = MSAlg_morph (S,A,j9,j9) ) by Def4, MSUALG_3:9; hence A39: e in the Arrows of (MSAlgCat (S,A)) . (j,j) by A38, Def3; ::_thesis: for b1 being Element of the carrier of (MSAlgCat (S,A)) for b2 being set holds ( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 ) let i be Element of (MSAlgCat (S,A)); ::_thesis: for b1 being set holds ( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,b1) = b1 ) reconsider i9 = i as Element of MSAlg_set (S,A) by Def4; let f be set ; ::_thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f ) reconsider I = i, J = j as object of (MSAlgCat (S,A)) ; assume A40: f in the Arrows of (MSAlgCat (S,A)) . (i,j) ; ::_thesis: ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f then f in MSAlg_morph (S,A,i9,j9) by Def4; then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that M1 = i9 and A41: N1 = j9 and A42: F = f and the Sorts of M1 is_transformable_to the Sorts of N1 and F is_homomorphism M1,N1 by Def3; reconsider F = F as ManySortedFunction of M1,MS by A38, A41; ( the Comp of (MSAlgCat (S,A)) . (I,J,J)) . (e,f) = e ** F by A39, A40, A42, Def4; hence ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f by A42, MSUALG_3:4; ::_thesis: verum end; thus the Comp of (MSAlgCat (S,A)) is with_right_units ::_thesis: verum proof let i be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st ( b1 in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b2 being Element of the carrier of (MSAlgCat (S,A)) for b3 being set holds ( not b3 in the Arrows of (MSAlgCat (S,A)) . (i,b2) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b2)) . (b3,b1) = b3 ) ) ) reconsider i9 = i as Element of MSAlg_set (S,A) by Def4; consider MS being strict feasible MSAlgebra over S such that A43: MS = i9 and for C being Component of the Sorts of MS holds C c= A by Def2; reconsider e = id the Sorts of MS as ManySortedFunction of MS,MS ; take e ; ::_thesis: ( e in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b1 being Element of the carrier of (MSAlgCat (S,A)) for b2 being set holds ( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 ) ) ) ( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (i,i) = MSAlg_morph (S,A,i9,i9) ) by Def4, MSUALG_3:9; hence A44: e in the Arrows of (MSAlgCat (S,A)) . (i,i) by A43, Def3; ::_thesis: for b1 being Element of the carrier of (MSAlgCat (S,A)) for b2 being set holds ( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 ) let j be Element of (MSAlgCat (S,A)); ::_thesis: for b1 being set holds ( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (b1,e) = b1 ) reconsider j9 = j as Element of MSAlg_set (S,A) by Def4; let f be set ; ::_thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f ) reconsider I = i, J = j as object of (MSAlgCat (S,A)) ; assume A45: f in the Arrows of (MSAlgCat (S,A)) . (i,j) ; ::_thesis: ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f then f in MSAlg_morph (S,A,i9,j9) by Def4; then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that A46: M1 = i9 and N1 = j9 and A47: F = f and the Sorts of M1 is_transformable_to the Sorts of N1 and F is_homomorphism M1,N1 by Def3; reconsider F = F as ManySortedFunction of MS,N1 by A43, A46; ( the Comp of (MSAlgCat (S,A)) . (I,I,J)) . (f,e) = F ** e by A44, A45, A47, Def4; hence ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f by A47, MSUALG_3:3; ::_thesis: verum end; end; end; theorem :: MSINST_1:6 for A being non empty set for S being non empty non void ManySortedSign for C being category st C = MSAlgCat (S,A) holds for o being object of C holds o is strict feasible MSAlgebra over S proof let A be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for C being category st C = MSAlgCat (S,A) holds for o being object of C holds o is strict feasible MSAlgebra over S let S be non empty non void ManySortedSign ; ::_thesis: for C being category st C = MSAlgCat (S,A) holds for o being object of C holds o is strict feasible MSAlgebra over S let C be category; ::_thesis: ( C = MSAlgCat (S,A) implies for o being object of C holds o is strict feasible MSAlgebra over S ) assume A1: C = MSAlgCat (S,A) ; ::_thesis: for o being object of C holds o is strict feasible MSAlgebra over S let o be object of C; ::_thesis: o is strict feasible MSAlgebra over S o in the carrier of C ; then o in MSAlg_set (S,A) by A1, Def4; then ex M being strict feasible MSAlgebra over S st ( o = M & ( for C1 being Component of the Sorts of M holds C1 c= A ) ) by Def2; hence o is strict feasible MSAlgebra over S ; ::_thesis: verum end;