:: MSUALG_2 semantic presentation begin registration let I be set ; let X be ManySortedSet of I; let Y be V8() ManySortedSet of I; clusterX \/ Y -> V8() ; coherence X \/ Y is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (X \/ Y) . i is empty ) assume A1: i in I ; ::_thesis: not (X \/ Y) . i is empty then (X \/ Y) . i = (X . i) \/ (Y . i) by PBOOLE:def_4; hence not (X \/ Y) . i is empty by A1; ::_thesis: verum end; clusterY \/ X -> V8() ; coherence Y \/ X is non-empty ; end; theorem Th1: :: MSUALG_2:1 for I being non empty set for X, Y being ManySortedSet of I for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i)) proof let I be non empty set ; ::_thesis: for X, Y being ManySortedSet of I for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i)) let X, Y be ManySortedSet of I; ::_thesis: for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i)) let i be Element of I * ; ::_thesis: product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i)) A1: rng i c= I by FINSEQ_1:def_4; dom X = I by PARTFUN1:def_2; then A2: dom (X * i) = dom i by A1, RELAT_1:27; dom (X /\ Y) = I by PARTFUN1:def_2; then A3: dom ((X /\ Y) * i) = dom i by A1, RELAT_1:27; dom Y = I by PARTFUN1:def_2; then A4: dom (Y * i) = dom i by A1, RELAT_1:27; thus product ((X /\ Y) * i) c= (product (X * i)) /\ (product (Y * i)) :: according to XBOOLE_0:def_10 ::_thesis: (product (X * i)) /\ (product (Y * i)) c= product ((X /\ Y) * i) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ((X /\ Y) * i) or x in (product (X * i)) /\ (product (Y * i)) ) assume x in product ((X /\ Y) * i) ; ::_thesis: x in (product (X * i)) /\ (product (Y * i)) then consider g being Function such that A5: ( x = g & dom g = dom ((X /\ Y) * i) ) and A6: for y being set st y in dom ((X /\ Y) * i) holds g . y in ((X /\ Y) * i) . y by CARD_3:def_5; for y being set st y in dom (Y * i) holds g . y in (Y * i) . y proof let y be set ; ::_thesis: ( y in dom (Y * i) implies g . y in (Y * i) . y ) assume A7: y in dom (Y * i) ; ::_thesis: g . y in (Y * i) . y then g . y in ((X /\ Y) * i) . y by A4, A3, A6; then A8: g . y in (X /\ Y) . (i . y) by A4, A3, A7, FUNCT_1:12; i . y in rng i by A4, A7, FUNCT_1:def_3; then g . y in (X . (i . y)) /\ (Y . (i . y)) by A1, A8, PBOOLE:def_5; then g . y in Y . (i . y) by XBOOLE_0:def_4; hence g . y in (Y * i) . y by A7, FUNCT_1:12; ::_thesis: verum end; then A9: x in product (Y * i) by A4, A3, A5, CARD_3:def_5; for y being set st y in dom (X * i) holds g . y in (X * i) . y proof let y be set ; ::_thesis: ( y in dom (X * i) implies g . y in (X * i) . y ) assume A10: y in dom (X * i) ; ::_thesis: g . y in (X * i) . y then g . y in ((X /\ Y) * i) . y by A2, A3, A6; then A11: g . y in (X /\ Y) . (i . y) by A2, A3, A10, FUNCT_1:12; i . y in rng i by A2, A10, FUNCT_1:def_3; then g . y in (X . (i . y)) /\ (Y . (i . y)) by A1, A11, PBOOLE:def_5; then g . y in X . (i . y) by XBOOLE_0:def_4; hence g . y in (X * i) . y by A10, FUNCT_1:12; ::_thesis: verum end; then x in product (X * i) by A2, A3, A5, CARD_3:def_5; hence x in (product (X * i)) /\ (product (Y * i)) by A9, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (product (X * i)) /\ (product (Y * i)) or x in product ((X /\ Y) * i) ) assume A12: x in (product (X * i)) /\ (product (Y * i)) ; ::_thesis: x in product ((X /\ Y) * i) then x in product (X * i) by XBOOLE_0:def_4; then consider g being Function such that A13: x = g and A14: dom g = dom (X * i) and A15: for y being set st y in dom (X * i) holds g . y in (X * i) . y by CARD_3:def_5; x in product (Y * i) by A12, XBOOLE_0:def_4; then A16: ex h being Function st ( x = h & dom h = dom (Y * i) & ( for y being set st y in dom (Y * i) holds h . y in (Y * i) . y ) ) by CARD_3:def_5; for y being set st y in dom ((X /\ Y) * i) holds g . y in ((X /\ Y) * i) . y proof let y be set ; ::_thesis: ( y in dom ((X /\ Y) * i) implies g . y in ((X /\ Y) * i) . y ) assume A17: y in dom ((X /\ Y) * i) ; ::_thesis: g . y in ((X /\ Y) * i) . y then A18: i . y in rng i by A3, FUNCT_1:def_3; g . y in (X * i) . y by A2, A3, A15, A17; then A19: g . y in X . (i . y) by A2, A3, A17, FUNCT_1:12; g . y in (Y * i) . y by A4, A3, A13, A16, A17; then g . y in Y . (i . y) by A4, A3, A17, FUNCT_1:12; then g . y in (X . (i . y)) /\ (Y . (i . y)) by A19, XBOOLE_0:def_4; then g . y in (X /\ Y) . (i . y) by A1, A18, PBOOLE:def_5; hence g . y in ((X /\ Y) * i) . y by A17, FUNCT_1:12; ::_thesis: verum end; hence x in product ((X /\ Y) * i) by A2, A3, A13, A14, CARD_3:def_5; ::_thesis: verum end; begin definition let S be non empty ManySortedSign ; let U0 be MSAlgebra over S; mode MSSubset of U0 is ManySortedSubset of the Sorts of U0; end; definition let S be non empty ManySortedSign ; let IT be SortSymbol of S; attrIT is with_const_op means :Def1: :: MSUALG_2:def 1 ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = IT ); end; :: deftheorem Def1 defines with_const_op MSUALG_2:def_1_:_ for S being non empty ManySortedSign for IT being SortSymbol of S holds ( IT is with_const_op iff ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = IT ) ); definition let IT be non empty ManySortedSign ; attrIT is all-with_const_op means :Def2: :: MSUALG_2:def 2 for s being SortSymbol of IT holds s is with_const_op ; end; :: deftheorem Def2 defines all-with_const_op MSUALG_2:def_2_:_ for IT being non empty ManySortedSign holds ( IT is all-with_const_op iff for s being SortSymbol of IT holds s is with_const_op ); registration let A be non empty set ; let B be set ; let a be Function of B,(A *); let r be Function of B,A; cluster ManySortedSign(# A,B,a,r #) -> non empty ; coherence not ManySortedSign(# A,B,a,r #) is empty ; end; registration cluster non empty non void V60() strict all-with_const_op for ManySortedSign ; existence ex b1 being non empty ManySortedSign st ( not b1 is void & b1 is all-with_const_op & b1 is strict ) proof set x = the set ; set C = { the set }; consider a being Function such that A1: dom a = { the set } and A2: rng a = {(<*> { the set })} by FUNCT_1:5; rng a c= { the set } * proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng a or y in { the set } * ) assume y in rng a ; ::_thesis: y in { the set } * then y = <*> { the set } by A2, TARSKI:def_1; hence y in { the set } * by FINSEQ_1:def_11; ::_thesis: verum end; then reconsider a = a as Function of { the set },({ the set } *) by A1, FUNCT_2:def_1, RELSET_1:4; consider r being Function such that A3: dom r = { the set } and A4: rng r = { the set } by FUNCT_1:5; reconsider r = r as Function of { the set },{ the set } by A3, A4, FUNCT_2:def_1, RELSET_1:4; set M = ManySortedSign(# { the set },{ the set },a,r #); take ManySortedSign(# { the set },{ the set },a,r #) ; ::_thesis: ( not ManySortedSign(# { the set },{ the set },a,r #) is void & ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op & ManySortedSign(# { the set },{ the set },a,r #) is strict ) thus not ManySortedSign(# { the set },{ the set },a,r #) is void ; ::_thesis: ( ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op & ManySortedSign(# { the set },{ the set },a,r #) is strict ) for s being SortSymbol of ManySortedSign(# { the set },{ the set },a,r #) holds s is with_const_op proof reconsider o = the set as OperSymbol of ManySortedSign(# { the set },{ the set },a,r #) by TARSKI:def_1; let s be SortSymbol of ManySortedSign(# { the set },{ the set },a,r #); ::_thesis: s is with_const_op take o ; :: according to MSUALG_2:def_1 ::_thesis: ( the Arity of ManySortedSign(# { the set },{ the set },a,r #) . o = {} & the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s ) a . o in rng a by A1, FUNCT_1:def_3; hence the Arity of ManySortedSign(# { the set },{ the set },a,r #) . o = {} by A2, TARSKI:def_1; ::_thesis: the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s ( s = the set & r . o in rng r ) by A3, FUNCT_1:def_3, TARSKI:def_1; hence the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s by A4, TARSKI:def_1; ::_thesis: verum end; hence ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op by Def2; ::_thesis: ManySortedSign(# { the set },{ the set },a,r #) is strict thus ManySortedSign(# { the set },{ the set },a,r #) is strict ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let s be SortSymbol of S; func Constants (U0,s) -> Subset of ( the Sorts of U0 . s) means :Def3: :: MSUALG_2:def 3 ex A being non empty set st ( A = the Sorts of U0 . s & it = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) if the Sorts of U0 . s <> {} otherwise it = {} ; existence ( ( the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) ex A being non empty set st ( A = the Sorts of U0 . s & b1 = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) & ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} ) ) proof hereby ::_thesis: ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} ) assume the Sorts of U0 . s <> {} ; ::_thesis: ex E being Subset of ( the Sorts of U0 . s) ex A being non empty set st ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) then reconsider A = the Sorts of U0 . s as non empty set ; set E = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ; { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } or x in A ) assume x in { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ; ::_thesis: x in A then ex w being Element of the Sorts of U0 . s st ( w = x & ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & w in rng (Den (o,U0)) ) ) ; hence x in A ; ::_thesis: verum end; then reconsider E = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } as Subset of ( the Sorts of U0 . s) ; take E = E; ::_thesis: ex A being non empty set st ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) take A = A; ::_thesis: ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) thus ( A = the Sorts of U0 . s & E = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ; ::_thesis: verum end; assume the Sorts of U0 . s = {} ; ::_thesis: ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} take {} ( the Sorts of U0 . s) ; ::_thesis: {} ( the Sorts of U0 . s) = {} thus {} ( the Sorts of U0 . s) = {} ; ::_thesis: verum end; correctness consistency for b1 being Subset of ( the Sorts of U0 . s) holds verum; uniqueness for b1, b2 being Subset of ( the Sorts of U0 . s) holds ( ( the Sorts of U0 . s <> {} & ex A being non empty set st ( A = the Sorts of U0 . s & b1 = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) & ex A being non empty set st ( A = the Sorts of U0 . s & b2 = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) implies b1 = b2 ) & ( not the Sorts of U0 . s <> {} & b1 = {} & b2 = {} implies b1 = b2 ) ); ; end; :: deftheorem Def3 defines Constants MSUALG_2:def_3_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for s being SortSymbol of S for b4 being Subset of ( the Sorts of U0 . s) holds ( ( the Sorts of U0 . s <> {} implies ( b4 = Constants (U0,s) iff ex A being non empty set st ( A = the Sorts of U0 . s & b4 = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) ) & ( not the Sorts of U0 . s <> {} implies ( b4 = Constants (U0,s) iff b4 = {} ) ) ); definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; func Constants U0 -> MSSubset of U0 means :Def4: :: MSUALG_2:def 4 for s being SortSymbol of S holds it . s = Constants (U0,s); existence ex b1 being MSSubset of U0 st for s being SortSymbol of S holds b1 . s = Constants (U0,s) proof deffunc H1( SortSymbol of S) -> Subset of ( the Sorts of U0 . \$1) = Constants (U0,\$1); consider f being Function such that A1: ( dom f = the carrier of S & ( for d being SortSymbol of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; f c= the Sorts of U0 proof let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or f . s c= the Sorts of U0 . s ) assume s in the carrier of S ; ::_thesis: f . s c= the Sorts of U0 . s then reconsider s1 = s as SortSymbol of S ; f . s1 = Constants (U0,s1) by A1; hence f . s c= the Sorts of U0 . s ; ::_thesis: verum end; then reconsider f = f as MSSubset of U0 by PBOOLE:def_18; take f ; ::_thesis: for s being SortSymbol of S holds f . s = Constants (U0,s) thus for s being SortSymbol of S holds f . s = Constants (U0,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds b2 . s = Constants (U0,s) ) holds b1 = b2 proof let W1, W2 be MSSubset of U0; ::_thesis: ( ( for s being SortSymbol of S holds W1 . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds W2 . s = Constants (U0,s) ) implies W1 = W2 ) assume that A2: for s being SortSymbol of S holds W1 . s = Constants (U0,s) and A3: for s being SortSymbol of S holds W2 . s = Constants (U0,s) ; ::_thesis: W1 = W2 for s being set st s in the carrier of S holds W1 . s = W2 . s proof let s be set ; ::_thesis: ( s in the carrier of S implies W1 . s = W2 . s ) assume s in the carrier of S ; ::_thesis: W1 . s = W2 . s then reconsider t = s as SortSymbol of S ; W1 . t = Constants (U0,t) by A2; hence W1 . s = W2 . s by A3; ::_thesis: verum end; hence W1 = W2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def4 defines Constants MSUALG_2:def_4_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for b3 being MSSubset of U0 holds ( b3 = Constants U0 iff for s being SortSymbol of S holds b3 . s = Constants (U0,s) ); registration let S be non empty non void all-with_const_op ManySortedSign ; let U0 be non-empty MSAlgebra over S; let s be SortSymbol of S; cluster Constants (U0,s) -> non empty ; coherence not Constants (U0,s) is empty proof ( dom {} = {} & rng {} = {} ) ; then reconsider a = {} as Function of {},{} by FUNCT_2:1; s is with_const_op by Def2; then consider o being OperSymbol of S such that A1: the Arity of S . o = {} and A2: the ResultSort of S . o = s by Def1; A3: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then ( dom ( the Sorts of U0 #) = the carrier of S * & the Arity of S . o in rng the Arity of S ) by FUNCT_1:def_3, PARTFUN1:def_2; then A4: o in dom (( the Sorts of U0 #) * the Arity of S) by A3, FUNCT_1:11; Args (o,U0) = (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4 .= ( the Sorts of U0 #) . ( the Arity of S . o) by A4, FUNCT_1:12 .= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def_1 .= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def_5 .= product ( the Sorts of U0 * a) by A1, MSUALG_1:def_1 .= {{}} by CARD_3:10 ; then A5: {} in Args (o,U0) by TARSKI:def_1; set f = Den (o,U0); A6: rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def_19; dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1; then A7: (Den (o,U0)) . {} in rng (Den (o,U0)) by A5, FUNCT_1:def_3; A8: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then ( dom the Sorts of U0 = the carrier of S & the ResultSort of S . o in rng the ResultSort of S ) by FUNCT_1:def_3, PARTFUN1:def_2; then A9: o in dom ( the Sorts of U0 * the ResultSort of S) by A8, FUNCT_1:11; Result (o,U0) = ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of U0 . s by A2, A9, FUNCT_1:12 ; then reconsider a = (Den (o,U0)) . {} as Element of the Sorts of U0 . s by A6, A7; ex A being non empty set st ( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } ) by Def3; then a in Constants (U0,s) by A1, A2, A7; hence not Constants (U0,s) is empty ; ::_thesis: verum end; end; registration let S be non empty non void all-with_const_op ManySortedSign ; let U0 be non-empty MSAlgebra over S; cluster Constants U0 -> V8() ; coherence Constants U0 is non-empty proof now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ not_(Constants_U0)_._i_is_empty let i be set ; ::_thesis: ( i in the carrier of S implies not (Constants U0) . i is empty ) assume i in the carrier of S ; ::_thesis: not (Constants U0) . i is empty then reconsider s = i as SortSymbol of S ; (Constants U0) . s = Constants (U0,s) by Def4; hence not (Constants U0) . i is empty ; ::_thesis: verum end; hence Constants U0 is non-empty by PBOOLE:def_13; ::_thesis: verum end; end; begin definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let o be OperSymbol of S; let A be MSSubset of U0; predA is_closed_on o means :Def5: :: MSUALG_2:def 5 rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o; end; :: deftheorem Def5 defines is_closed_on MSUALG_2:def_5_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for o being OperSymbol of S for A being MSSubset of U0 holds ( A is_closed_on o iff rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o ); definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; attrA is opers_closed means :Def6: :: MSUALG_2:def 6 for o being OperSymbol of S holds A is_closed_on o; end; :: deftheorem Def6 defines opers_closed MSUALG_2:def_6_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds ( A is opers_closed iff for o being OperSymbol of S holds A is_closed_on o ); theorem Th2: :: MSUALG_2:2 for S being non empty non void ManySortedSign for o being OperSymbol of S for U0 being MSAlgebra over S for B0, B1 being MSSubset of U0 st B0 c= B1 holds ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U0 being MSAlgebra over S for B0, B1 being MSSubset of U0 st B0 c= B1 holds ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o let o be OperSymbol of S; ::_thesis: for U0 being MSAlgebra over S for B0, B1 being MSSubset of U0 st B0 c= B1 holds ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o let U0 be MSAlgebra over S; ::_thesis: for B0, B1 being MSSubset of U0 st B0 c= B1 holds ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o let B0, B1 be MSSubset of U0; ::_thesis: ( B0 c= B1 implies ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o ) reconsider a = the Arity of S . o as Element of the carrier of S * ; A1: rng a c= the carrier of S by FINSEQ_1:def_4; A2: dom B0 = the carrier of S by PARTFUN1:def_2; then A3: dom (B0 * a) = dom a by A1, RELAT_1:27; assume A4: B0 c= B1 ; ::_thesis: ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o A5: for x being set st x in dom (B0 * a) holds (B0 * a) . x c= (B1 * a) . x proof let x be set ; ::_thesis: ( x in dom (B0 * a) implies (B0 * a) . x c= (B1 * a) . x ) assume A6: x in dom (B0 * a) ; ::_thesis: (B0 * a) . x c= (B1 * a) . x then a . x in rng a by A3, FUNCT_1:def_3; then B0 . (a . x) c= B1 . (a . x) by A4, A1, PBOOLE:def_2; then (B0 * a) . x c= B1 . (a . x) by A3, A6, FUNCT_1:13; hence (B0 * a) . x c= (B1 * a) . x by A3, A6, FUNCT_1:13; ::_thesis: verum end; A7: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then dom ((B0 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2; then ((B0 #) * the Arity of S) . o = (B0 #) . a by A7, FUNCT_1:12; then A8: ((B0 #) * the Arity of S) . o = product (B0 * a) by FINSEQ_2:def_5; dom ((B1 #) * the Arity of S) = dom the Arity of S by A7, PARTFUN1:def_2; then ((B1 #) * the Arity of S) . o = (B1 #) . a by A7, FUNCT_1:12; then A9: ((B1 #) * the Arity of S) . o = product (B1 * a) by FINSEQ_2:def_5; dom B1 = the carrier of S by PARTFUN1:def_2; then dom (B1 * a) = dom a by A1, RELAT_1:27; hence ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by A8, A9, A2, A1, A5, CARD_3:27, RELAT_1:27; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let o be OperSymbol of S; let A be MSSubset of U0; assume A1: A is_closed_on o ; funco /. A -> Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) equals :Def7: :: MSUALG_2:def 7 (Den (o,U0)) | (((A #) * the Arity of S) . o); coherence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) proof set f = (Den (o,U0)) | (((A #) * the Arity of S) . o); set B = the Sorts of U0; A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; percases ( (A * the ResultSort of S) . o = {} or (A * the ResultSort of S) . o <> {} ) ; supposeA3: (A * the ResultSort of S) . o = {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1, Def5; then A4: (Den (o,U0)) | (((A #) * the Arity of S) . o) = {} by A3; now__::_thesis:_(Den_(o,U0))_|_(((A_#)_*_the_Arity_of_S)_._o)_is_Function_of_(((A_#)_*_the_Arity_of_S)_._o),((A_*_the_ResultSort_of_S)_._o) percases ( ((A #) * the Arity of S) . o = {} or ((A #) * the Arity of S) . o <> {} ) ; suppose ((A #) * the Arity of S) . o = {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A4, RELSET_1:12; ::_thesis: verum end; suppose ((A #) * the Arity of S) . o <> {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) thus (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A3, A4, FUNCT_2:def_1, RELSET_1:12; ::_thesis: verum end; end; end; hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) ; ::_thesis: verum end; supposeA5: (A * the ResultSort of S) . o <> {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) reconsider B0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; A6: A c= B0 by PBOOLE:def_18; A7: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1, Def5; A c= the Sorts of U0 by PBOOLE:def_18; then A . ( the ResultSort of S . o) c= the Sorts of U0 . ( the ResultSort of S . o) by PBOOLE:def_2; then the Sorts of U0 . ( the ResultSort of S . o) <> {} by A2, A5, FUNCT_1:13; then ( the Sorts of U0 * the ResultSort of S) . o <> {} by A2, FUNCT_1:13; then Result (o,U0) <> {} by MSUALG_1:def_5; then dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1 .= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4 ; then dom ((Den (o,U0)) | (((A #) * the Arity of S) . o)) = ((( the Sorts of U0 #) * the Arity of S) . o) /\ (((A #) * the Arity of S) . o) by RELAT_1:61 .= ((A #) * the Arity of S) . o by A6, Th2, XBOOLE_1:28 ; hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A7, FUNCT_2:2; ::_thesis: verum end; end; end; end; :: deftheorem Def7 defines /. MSUALG_2:def_7_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for o being OperSymbol of S for A being MSSubset of U0 st A is_closed_on o holds o /. A = (Den (o,U0)) | (((A #) * the Arity of S) . o); definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; func Opers (U0,A) -> ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S means :Def8: :: MSUALG_2:def 8 for o being OperSymbol of S holds it . o = o /. A; existence ex b1 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st for o being OperSymbol of S holds b1 . o = o /. A proof set B = (A #) * the Arity of S; set C = A * the ResultSort of S; defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = o /. A; A1: for x being set st x in the carrier' of S holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] ) assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y] then reconsider o = x as OperSymbol of S ; take o /. A ; ::_thesis: S1[x,o /. A] thus S1[x,o /. A] ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider o = x as OperSymbol of S by A2; f . o = o /. A by A2; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6; for x being set st x in the carrier' of S holds f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) proof let x be set ; ::_thesis: ( x in the carrier' of S implies f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) ) assume x in the carrier' of S ; ::_thesis: f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) then reconsider o = x as OperSymbol of S ; f . o = o /. A by A2; hence f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = o /. A let o be OperSymbol of S; ::_thesis: f . o = o /. A thus f . o = o /. A by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = o /. A ) & ( for o being OperSymbol of S holds b2 . o = o /. A ) holds b1 = b2 proof let f1, f2 be ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f1 . o = o /. A ) & ( for o being OperSymbol of S holds f2 . o = o /. A ) implies f1 = f2 ) assume that A3: for o being OperSymbol of S holds f1 . o = o /. A and A4: for o being OperSymbol of S holds f2 . o = o /. A ; ::_thesis: f1 = f2 for x being set st x in the carrier' of S holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies f1 . x = f2 . x ) assume x in the carrier' of S ; ::_thesis: f1 . x = f2 . x then reconsider o1 = x as OperSymbol of S ; f1 . o1 = o1 /. A by A3; hence f1 . x = f2 . x by A4; ::_thesis: verum end; hence f1 = f2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def8 defines Opers MSUALG_2:def_8_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 for b4 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds ( b4 = Opers (U0,A) iff for o being OperSymbol of S holds b4 . o = o /. A ); theorem Th3: :: MSUALG_2:3 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) ) assume A1: B = the Sorts of U0 ; ::_thesis: ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) thus A2: B is opers_closed ::_thesis: for o being OperSymbol of S holds o /. B = Den (o,U0) proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o Result (o,U0) = (B * the ResultSort of S) . o by A1, MSUALG_1:def_5; hence rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by RELAT_1:def_19; :: according to MSUALG_2:def_5 ::_thesis: verum end; let o be OperSymbol of S; ::_thesis: o /. B = Den (o,U0) B is_closed_on o by A2, Def6; then A3: o /. B = (Den (o,U0)) | (((B #) * the Arity of S) . o) by Def7; percases ( (B * the ResultSort of S) . o = {} or (B * the ResultSort of S) . o <> {} ) ; suppose (B * the ResultSort of S) . o = {} ; ::_thesis: o /. B = Den (o,U0) then Result (o,U0) = {} by A1, MSUALG_1:def_5; then Den (o,U0) = {} ; hence o /. B = Den (o,U0) by A3; ::_thesis: verum end; suppose (B * the ResultSort of S) . o <> {} ; ::_thesis: o /. B = Den (o,U0) then Result (o,U0) <> {} by A1, MSUALG_1:def_5; then A4: dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1; Args (o,U0) = ((B #) * the Arity of S) . o by A1, MSUALG_1:def_4; hence o /. B = Den (o,U0) by A3, A4, RELAT_1:68; ::_thesis: verum end; end; end; theorem Th4: :: MSUALG_2:4 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds Opers (U0,B) = the Charact of U0 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds Opers (U0,B) = the Charact of U0 let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds Opers (U0,B) = the Charact of U0 let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Opers (U0,B) = the Charact of U0 ) set f1 = the Charact of U0; set f2 = Opers (U0,B); assume A1: B = the Sorts of U0 ; ::_thesis: Opers (U0,B) = the Charact of U0 for x being set st x in the carrier' of S holds the Charact of U0 . x = (Opers (U0,B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U0,B)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of U0 . x = (Opers (U0,B)) . x then reconsider o1 = x as OperSymbol of S ; ( the Charact of U0 . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def_6; hence the Charact of U0 . x = (Opers (U0,B)) . x by A1, Th3; ::_thesis: verum end; hence Opers (U0,B) = the Charact of U0 by PBOOLE:3; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; mode MSSubAlgebra of U0 -> MSAlgebra over S means :Def9: :: MSUALG_2:def 9 ( the Sorts of it is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of it holds ( B is opers_closed & the Charact of it = Opers (U0,B) ) ) ); existence ex b1 being MSAlgebra over S st ( the Sorts of b1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds ( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) ) proof take U1 = U0; ::_thesis: ( the Sorts of U1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) thus the Sorts of U1 is MSSubset of U0 by PBOOLE:def_18; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) set f1 = the Charact of U1; set f2 = Opers (U0,B); assume A1: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) hence B is opers_closed by Th3; ::_thesis: the Charact of U1 = Opers (U0,B) for x being set st x in the carrier' of S holds the Charact of U1 . x = (Opers (U0,B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U0,B)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of U1 . x = (Opers (U0,B)) . x then reconsider o1 = x as OperSymbol of S ; ( the Charact of U1 . o1 = Den (o1,U1) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def_6; hence the Charact of U1 . x = (Opers (U0,B)) . x by A1, Th3; ::_thesis: verum end; hence the Charact of U1 = Opers (U0,B) by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def9 defines MSSubAlgebra MSUALG_2:def_9_:_ for S being non empty non void ManySortedSign for U0, b3 being MSAlgebra over S holds ( b3 is MSSubAlgebra of U0 iff ( the Sorts of b3 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b3 holds ( B is opers_closed & the Charact of b3 = Opers (U0,B) ) ) ) ); Lm1: for S being non empty non void ManySortedSign for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 let U0 be MSAlgebra over S; ::_thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 reconsider A = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSAlgebra over S ; now__::_thesis:_(_the_Sorts_of_A_is_MSSubset_of_U0_&_(_for_B_being_MSSubset_of_U0_st_B_=_the_Sorts_of_A_holds_ (_B_is_opers_closed_&_the_Charact_of_A_=_Opers_(U0,B)_)_)_) thus the Sorts of A is MSSubset of U0 by PBOOLE:def_18; ::_thesis: for B being MSSubset of U0 st B = the Sorts of A holds ( B is opers_closed & the Charact of A = Opers (U0,B) ) let B be MSSubset of U0; ::_thesis: ( B = the Sorts of A implies ( B is opers_closed & the Charact of A = Opers (U0,B) ) ) set f1 = the Charact of A; set f2 = Opers (U0,B); assume A1: B = the Sorts of A ; ::_thesis: ( B is opers_closed & the Charact of A = Opers (U0,B) ) hence B is opers_closed by Th3; ::_thesis: the Charact of A = Opers (U0,B) for x being set st x in the carrier' of S holds the Charact of A . x = (Opers (U0,B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of A . x = (Opers (U0,B)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of A . x = (Opers (U0,B)) . x then reconsider o1 = x as Element of the carrier' of S ; ( the Charact of A . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def_6; hence the Charact of A . x = (Opers (U0,B)) . x by A1, Th3; ::_thesis: verum end; hence the Charact of A = Opers (U0,B) by PBOOLE:3; ::_thesis: verum end; hence MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Def9; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; cluster strict for MSSubAlgebra of U0; existence ex b1 being MSSubAlgebra of U0 st b1 is strict proof MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1; hence ex b1 being MSSubAlgebra of U0 st b1 is strict ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; cluster MSAlgebra(# the Sorts of U0, the Charact of U0 #) -> non-empty ; coherence MSAlgebra(# the Sorts of U0, the Charact of U0 #) is non-empty by MSUALG_1:def_3; end; registration let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; cluster strict non-empty for MSSubAlgebra of U0; existence ex b1 being MSSubAlgebra of U0 st ( b1 is non-empty & b1 is strict ) proof MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1; hence ex b1 being MSSubAlgebra of U0 st ( b1 is non-empty & b1 is strict ) ; ::_thesis: verum end; end; theorem :: MSUALG_2:5 for S being non empty non void ManySortedSign for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds U0 is MSSubAlgebra of U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds U0 is MSSubAlgebra of U1 let U0, U1 be MSAlgebra over S; ::_thesis: ( MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) implies U0 is MSSubAlgebra of U1 ) assume A1: MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) ; ::_thesis: U0 is MSSubAlgebra of U1 hence the Sorts of U0 is MSSubset of U1 by PBOOLE:def_18; :: according to MSUALG_2:def_9 ::_thesis: for B being MSSubset of U1 st B = the Sorts of U0 holds ( B is opers_closed & the Charact of U0 = Opers (U1,B) ) let B be MSSubset of U1; ::_thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers (U1,B) ) ) set f1 = the Charact of U0; set f2 = Opers (U1,B); assume A2: B = the Sorts of U0 ; ::_thesis: ( B is opers_closed & the Charact of U0 = Opers (U1,B) ) thus B is opers_closed ::_thesis: the Charact of U0 = Opers (U1,B) proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o (Den (o,U1)) | (((B #) * the Arity of S) . o) c= Den (o,U1) by RELAT_1:59; then ( rng ((Den (o,U1)) | (((B #) * the Arity of S) . o)) c= rng (Den (o,U1)) & rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = (B * the ResultSort of S) . o ) by A1, A2, RELAT_1:11, RELAT_1:def_19, MSUALG_1:def_5; hence rng ((Den (o,U1)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by XBOOLE_1:1; :: according to MSUALG_2:def_5 ::_thesis: verum end; for x being set st x in the carrier' of S holds the Charact of U0 . x = (Opers (U1,B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U1,B)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of U0 . x = (Opers (U1,B)) . x then reconsider o1 = x as OperSymbol of S ; thus the Charact of U0 . x = (Opers (U1,B)) . x by A1, A2, Th4; ::_thesis: verum end; hence the Charact of U0 = Opers (U1,B) by PBOOLE:3; ::_thesis: verum end; theorem :: MSUALG_2:6 for S being non empty non void ManySortedSign for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds U0 is MSSubAlgebra of U2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds U0 is MSSubAlgebra of U2 let U0, U1, U2 be MSAlgebra over S; ::_thesis: ( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2 ) assume that A1: U0 is MSSubAlgebra of U1 and A2: U1 is MSSubAlgebra of U2 ; ::_thesis: U0 is MSSubAlgebra of U2 reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1, Def9; A3: B0 is opers_closed by A1, Def9; reconsider B1 = the Sorts of U1 as MSSubset of U2 by A2, Def9; A4: B1 is opers_closed by A2, Def9; reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def_18; A5: the Charact of U1 = Opers (U2,B1) by A2, Def9; the Sorts of U0 is MSSubset of U1 by A1, Def9; then A6: the Sorts of U0 c= the Sorts of U1 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U2 by A2, Def9; then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def_18; then the Sorts of U0 c= the Sorts of U2 by A6, PBOOLE:13; hence the Sorts of U0 is MSSubset of U2 by PBOOLE:def_18; :: according to MSUALG_2:def_9 ::_thesis: for B being MSSubset of U2 st B = the Sorts of U0 holds ( B is opers_closed & the Charact of U0 = Opers (U2,B) ) let B be MSSubset of U2; ::_thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers (U2,B) ) ) set O = the Charact of U0; set P = Opers (U2,B); A7: the Charact of U0 = Opers (U1,B0) by A1, Def9; assume A8: B = the Sorts of U0 ; ::_thesis: ( B is opers_closed & the Charact of U0 = Opers (U2,B) ) A9: for o being OperSymbol of S holds B is_closed_on o proof let o be OperSymbol of S; ::_thesis: B is_closed_on o A10: B0 is_closed_on o by A3, Def6; A11: B1 is_closed_on o by A4, Def6; A12: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def_6 .= o /. B1 by Def8 .= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A11, Def7 ; A13: ((B0 #) * the Arity of S) . o c= ((B19 #) * the Arity of S) . o by A6, Th2; Den (o,U0) = (Opers (U1,B0)) . o by A7, MSUALG_1:def_6 .= o /. B0 by Def8 .= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A10, A12, Def7 .= (Den (o,U2)) | ((((B1 #) * the Arity of S) . o) /\ (((B0 #) * the Arity of S) . o)) by RELAT_1:71 .= (Den (o,U2)) | (((B0 #) * the Arity of S) . o) by A13, XBOOLE_1:28 ; then rng ((Den (o,U2)) | (((B0 #) * the Arity of S) . o)) c= Result (o,U0) by RELAT_1:def_19; then rng ((Den (o,U2)) | (((B0 #) * the Arity of S) . o)) c= ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5; hence B is_closed_on o by A8, Def5; ::_thesis: verum end; hence B is opers_closed by Def6; ::_thesis: the Charact of U0 = Opers (U2,B) for x being set st x in the carrier' of S holds the Charact of U0 . x = (Opers (U2,B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U2,B)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of U0 . x = (Opers (U2,B)) . x then reconsider o = x as OperSymbol of S ; A14: B0 is_closed_on o by A3, Def6; A15: B1 is_closed_on o by A4, Def6; A16: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def_6 .= o /. B1 by Def8 .= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A15, Def7 ; thus the Charact of U0 . x = o /. B0 by A7, Def8 .= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A14, A16, Def7 .= (Den (o,U2)) | ((((B1 #) * the Arity of S) . o) /\ (((B0 #) * the Arity of S) . o)) by RELAT_1:71 .= (Den (o,U2)) | (((B #) * the Arity of S) . o) by A6, A8, Th2, XBOOLE_1:28 .= o /. B by A9, Def7 .= (Opers (U2,B)) . x by Def8 ; ::_thesis: verum end; hence the Charact of U0 = Opers (U2,B) by PBOOLE:3; ::_thesis: verum end; theorem Th7: :: MSUALG_2:7 for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) let U1, U2 be MSAlgebra over S; ::_thesis: ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) assume that A1: U1 is MSSubAlgebra of U2 and A2: U2 is MSSubAlgebra of U1 ; ::_thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) the Sorts of U2 is MSSubset of U1 by A2, Def9; then A3: the Sorts of U2 c= the Sorts of U1 by PBOOLE:def_18; reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def9; A4: the Charact of U1 = Opers (U2,B1) by A1, Def9; reconsider B2 = the Sorts of U2 as MSSubset of U1 by A2, Def9; A5: the Charact of U2 = Opers (U1,B2) by A2, Def9; the Sorts of U1 is MSSubset of U2 by A1, Def9; then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def_18; then A6: the Sorts of U1 = the Sorts of U2 by A3, PBOOLE:146; set O = the Charact of U1; set P = Opers (U1,B2); A7: B1 is opers_closed by A1, Def9; for x being set st x in the carrier' of S holds the Charact of U1 . x = (Opers (U1,B2)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U1,B2)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of U1 . x = (Opers (U1,B2)) . x then reconsider o = x as OperSymbol of S ; A8: Args (o,U2) = ((B2 #) * the Arity of S) . o by MSUALG_1:def_4; A9: B1 is_closed_on o by A7, Def6; thus the Charact of U1 . x = o /. B1 by A4, Def8 .= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A9, Def7 .= Den (o,U2) by A6, A8, RELSET_1:19 .= (Opers (U1,B2)) . x by A5, MSUALG_1:def_6 ; ::_thesis: verum end; hence MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A6, A5, PBOOLE:3; ::_thesis: verum end; theorem Th8: :: MSUALG_2:8 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds U1 is MSSubAlgebra of U2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds U1 is MSSubAlgebra of U2 let U0 be MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds U1 is MSSubAlgebra of U2 let U1, U2 be MSSubAlgebra of U0; ::_thesis: ( the Sorts of U1 c= the Sorts of U2 implies U1 is MSSubAlgebra of U2 ) reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as MSSubset of U0 by Def9; assume A1: the Sorts of U1 c= the Sorts of U2 ; ::_thesis: U1 is MSSubAlgebra of U2 hence the Sorts of U1 is MSSubset of U2 by PBOOLE:def_18; :: according to MSUALG_2:def_9 ::_thesis: for B being MSSubset of U2 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U2,B) ) let B be MSSubset of U2; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U2,B) ) ) A2: B1 is opers_closed by Def9; set O = the Charact of U1; set P = Opers (U2,B); A3: the Charact of U1 = Opers (U0,B1) by Def9; A4: B2 is opers_closed by Def9; A5: the Charact of U2 = Opers (U0,B2) by Def9; assume A6: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U2,B) ) A7: for o being OperSymbol of S holds B is_closed_on o proof let o be OperSymbol of S; ::_thesis: B is_closed_on o A8: B1 is_closed_on o by A2, Def6; A9: B2 is_closed_on o by A4, Def6; A10: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def_6 .= o /. B2 by Def8 .= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A9, Def7 ; Den (o,U1) = (Opers (U0,B1)) . o by A3, MSUALG_1:def_6 .= o /. B1 by Def8 .= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A8, Def7 .= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28 .= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A10, RELAT_1:71 ; then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= Result (o,U1) by RELAT_1:def_19; then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5; hence B is_closed_on o by A6, Def5; ::_thesis: verum end; hence B is opers_closed by Def6; ::_thesis: the Charact of U1 = Opers (U2,B) for x being set st x in the carrier' of S holds the Charact of U1 . x = (Opers (U2,B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U2,B)) . x ) assume x in the carrier' of S ; ::_thesis: the Charact of U1 . x = (Opers (U2,B)) . x then reconsider o = x as OperSymbol of S ; A11: B1 is_closed_on o by A2, Def6; A12: B2 is_closed_on o by A4, Def6; A13: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def_6 .= o /. B2 by Def8 .= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A12, Def7 ; thus the Charact of U1 . x = o /. B1 by A3, Def8 .= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A11, Def7 .= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28 .= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A13, RELAT_1:71 .= o /. B by A6, A7, Def7 .= (Opers (U2,B)) . x by Def8 ; ::_thesis: verum end; hence the Charact of U1 = Opers (U2,B) by PBOOLE:3; ::_thesis: verum end; theorem Th9: :: MSUALG_2:9 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) let U0 be MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) let U1, U2 be MSSubAlgebra of U0; ::_thesis: ( the Sorts of U1 = the Sorts of U2 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) assume the Sorts of U1 = the Sorts of U2 ; ::_thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) then ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 ) by Th8; hence MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by Th7; ::_thesis: verum end; theorem Th10: :: MSUALG_2:10 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1 let U0 be MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1 let U1 be MSSubAlgebra of U0; ::_thesis: Constants U0 is MSSubset of U1 Constants U0 c= the Sorts of U1 proof let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S or (Constants U0) . x c= the Sorts of U1 . x ) assume x in the carrier of S ; ::_thesis: (Constants U0) . x c= the Sorts of U1 . x then reconsider s = x as SortSymbol of S ; thus (Constants U0) . x c= the Sorts of U1 . x ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) percases ( the Sorts of U0 . s = {} or the Sorts of U0 . s <> {} ) ; supposeA1: the Sorts of U0 . s = {} ; ::_thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) (Constants U0) . s = Constants (U0,s) by Def4 .= {} by A1 ; hence ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) ; ::_thesis: verum end; suppose the Sorts of U0 . s <> {} ; ::_thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) then A2: ex A being non empty set st ( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } ) by Def3; reconsider u1 = the Sorts of U1 as MSSubset of U0 by Def9; assume A3: y in (Constants U0) . x ; ::_thesis: y in the Sorts of U1 . x (Constants U0) . x = Constants (U0,s) by Def4; then consider b being Element of the Sorts of U0 . s such that A4: b = y and A5: ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) by A3, A2; consider o being OperSymbol of S such that A6: the Arity of S . o = {} and A7: the ResultSort of S . o = s and A8: b in rng (Den (o,U0)) by A5; A9: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then A10: the Arity of S . o in rng the Arity of S by FUNCT_1:def_3; ( dom {} = {} & rng {} = {} ) ; then reconsider a = {} as Function of {},{} by FUNCT_2:1; A11: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; dom (u1 #) = the carrier of S * by PARTFUN1:def_2; then o in dom ((u1 #) * the Arity of S) by A9, A10, FUNCT_1:11; then A12: ((u1 #) * the Arity of S) . o = (u1 #) . ( the Arity of S . o) by FUNCT_1:12 .= (u1 #) . (the_arity_of o) by MSUALG_1:def_1 .= product (u1 * (the_arity_of o)) by FINSEQ_2:def_5 .= product (u1 * a) by A6, MSUALG_1:def_1 .= {{}} by CARD_3:10 ; dom ( the Sorts of U0 #) = the carrier of S * by PARTFUN1:def_2; then A13: o in dom (( the Sorts of U0 #) * the Arity of S) by A9, A10, FUNCT_1:11; u1 is opers_closed by Def9; then u1 is_closed_on o by Def6; then A14: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by Def5; rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def_19; then dom (Den (o,U0)) = Args (o,U0) by A8, FUNCT_2:def_1 .= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4 .= ( the Sorts of U0 #) . ( the Arity of S . o) by A13, FUNCT_1:12 .= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def_1 .= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def_5 .= product ( the Sorts of U0 * a) by A6, MSUALG_1:def_1 .= {{}} by CARD_3:10 ; then (Den (o,U0)) | (((u1 #) * the Arity of S) . o) = Den (o,U0) by A12, RELAT_1:68; then b in (u1 * the ResultSort of S) . o by A8, A14; hence y in the Sorts of U1 . x by A4, A7, A11, FUNCT_1:13; ::_thesis: verum end; end; end; end; hence Constants U0 is MSSubset of U1 by PBOOLE:def_18; ::_thesis: verum end; theorem :: MSUALG_2:11 for S being non empty non void all-with_const_op ManySortedSign for U0 being non-empty MSAlgebra over S for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V8() MSSubset of U1 by Th10; theorem :: MSUALG_2:12 for S being non empty non void all-with_const_op ManySortedSign for U0 being non-empty MSAlgebra over S for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is V8() proof let S be non empty non void all-with_const_op ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is V8() let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is V8() let U1, U2 be non-empty MSSubAlgebra of U0; ::_thesis: the Sorts of U1 /\ the Sorts of U2 is V8() Constants U0 is V8() MSSubset of U2 by Th10; then A1: Constants U0 c= the Sorts of U2 by PBOOLE:def_18; Constants U0 is V8() MSSubset of U1 by Th10; then Constants U0 c= the Sorts of U1 by PBOOLE:def_18; then A2: (Constants U0) /\ (Constants U0) c= the Sorts of U1 /\ the Sorts of U2 by A1, PBOOLE:21; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ not_(_the_Sorts_of_U1_/\_the_Sorts_of_U2)_._i_is_empty let i be set ; ::_thesis: ( i in the carrier of S implies not ( the Sorts of U1 /\ the Sorts of U2) . i is empty ) assume i in the carrier of S ; ::_thesis: not ( the Sorts of U1 /\ the Sorts of U2) . i is empty then reconsider s = i as SortSymbol of S ; ( the Sorts of U1 /\ the Sorts of U2) . s = ( the Sorts of U1 . s) /\ ( the Sorts of U2 . s) by PBOOLE:def_5; then A3: (Constants U0) . s c= ( the Sorts of U1 . s) /\ ( the Sorts of U2 . s) by A2, PBOOLE:def_2; ex a being set st a in (Constants U0) . s by XBOOLE_0:def_1; hence not ( the Sorts of U1 /\ the Sorts of U2) . i is empty by A3, PBOOLE:def_5; ::_thesis: verum end; hence the Sorts of U1 /\ the Sorts of U2 is V8() by PBOOLE:def_13; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; func SubSort A -> set means :Def10: :: MSUALG_2:def 10 for x being set holds ( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) proof defpred S1[ set ] means ( \$1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = \$1 holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ); consider X being set such that A1: for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) thus for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & \$1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = \$1 holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def10 defines SubSort MSUALG_2:def_10_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 for b4 being set holds ( b4 = SubSort A iff for x being set holds ( x in b4 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ); Lm2: for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds the Sorts of U0 in SubSort A proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 holds the Sorts of U0 in SubSort A let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds the Sorts of U0 in SubSort A let A be MSSubset of U0; ::_thesis: the Sorts of U0 in SubSort A set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0))); Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def_4; then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def_2, ZFMISC_1:82; then A1: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def_2; ( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds ( B is opers_closed & Constants U0 c= B & A c= B ) ) ) by Th3, PBOOLE:def_18; hence the Sorts of U0 in SubSort A by A1, Def10; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; cluster SubSort A -> non empty ; coherence not SubSort A is empty by Lm2; end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; func SubSort U0 -> set means :Def11: :: MSUALG_2:def 11 for x being set holds ( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) proof defpred S1[ set ] means ( \$1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = \$1 holds B is opers_closed ) ); consider X being set such that A1: for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) thus for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & \$1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = \$1 holds B is opers_closed ) ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def11 defines SubSort MSUALG_2:def_11_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for b3 being set holds ( b3 = SubSort U0 iff for x being set holds ( x in b3 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds B is opers_closed ) ) ) ); registration let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; cluster SubSort U0 -> non empty ; coherence not SubSort U0 is empty proof set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0))); defpred S1[ set ] means ( S is MSSubset of U0 & ( for B being MSSubset of U0 st B = S holds B is opers_closed ) ); consider X being set such that A1: for x being set holds ( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S1[x] ) ) from XBOOLE_0:sch_1(); Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def_4; then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def_2, ZFMISC_1:82; then A2: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def_2; ( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds B is opers_closed ) ) by Th3, PBOOLE:def_18; then reconsider X = X as non empty set by A1, A2; SubSort U0 = X by A1, Def11; hence not SubSort U0 is empty ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let e be Element of SubSort U0; func @ e -> MSSubset of U0 equals :: MSUALG_2:def 12 e; coherence e is MSSubset of U0 by Def11; end; :: deftheorem defines @ MSUALG_2:def_12_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for e being Element of SubSort U0 holds @ e = e; theorem Th13: :: MSUALG_2:13 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A, B being MSSubset of U0 holds ( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A, B being MSSubset of U0 holds ( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) ) let U0 be MSAlgebra over S; ::_thesis: for A, B being MSSubset of U0 holds ( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) ) let A, B be MSSubset of U0; ::_thesis: ( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) ) set C = bool (Union the Sorts of U0); A1: dom B = the carrier of S by PARTFUN1:def_2; A2: dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2; union (rng B) c= union (rng the Sorts of U0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng B) or x in union (rng the Sorts of U0) ) assume x in union (rng B) ; ::_thesis: x in union (rng the Sorts of U0) then consider Y being set such that A3: x in Y and A4: Y in rng B by TARSKI:def_4; consider y being set such that A5: y in dom B and A6: B . y = Y by A4, FUNCT_1:def_3; A7: the Sorts of U0 . y in rng the Sorts of U0 by A1, A2, A5, FUNCT_1:def_3; B c= the Sorts of U0 by PBOOLE:def_18; then B . y c= the Sorts of U0 . y by A1, A5, PBOOLE:def_2; hence x in union (rng the Sorts of U0) by A3, A6, A7, TARSKI:def_4; ::_thesis: verum end; then bool (union (rng B)) c= bool (union (rng the Sorts of U0)) by ZFMISC_1:67; then A8: bool (union (rng B)) c= bool (Union the Sorts of U0) by CARD_3:def_4; thus ( B in SubSort A implies ( B is opers_closed & Constants U0 c= B & A c= B ) ) by Def10; ::_thesis: ( B is opers_closed & Constants U0 c= B & A c= B implies B in SubSort A ) assume ( B is opers_closed & Constants U0 c= B & A c= B ) ; ::_thesis: B in SubSort A then A9: for C being MSSubset of U0 st C = B holds ( C is opers_closed & Constants U0 c= C & A c= C ) ; rng B c= bool (union (rng B)) by ZFMISC_1:82; then rng B c= bool (Union the Sorts of U0) by A8, XBOOLE_1:1; then B in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by A1, FUNCT_2:def_2; hence B in SubSort A by A9, Def10; ::_thesis: verum end; theorem Th14: :: MSUALG_2:14 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for B being MSSubset of U0 holds ( B in SubSort U0 iff B is opers_closed ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for B being MSSubset of U0 holds ( B in SubSort U0 iff B is opers_closed ) let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 holds ( B in SubSort U0 iff B is opers_closed ) let B be MSSubset of U0; ::_thesis: ( B in SubSort U0 iff B is opers_closed ) set C = bool (Union the Sorts of U0); A1: dom B = the carrier of S by PARTFUN1:def_2; A2: dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2; union (rng B) c= union (rng the Sorts of U0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng B) or x in union (rng the Sorts of U0) ) assume x in union (rng B) ; ::_thesis: x in union (rng the Sorts of U0) then consider Y being set such that A3: x in Y and A4: Y in rng B by TARSKI:def_4; consider y being set such that A5: y in dom B and A6: B . y = Y by A4, FUNCT_1:def_3; A7: the Sorts of U0 . y in rng the Sorts of U0 by A1, A2, A5, FUNCT_1:def_3; B c= the Sorts of U0 by PBOOLE:def_18; then B . y c= the Sorts of U0 . y by A1, A5, PBOOLE:def_2; hence x in union (rng the Sorts of U0) by A3, A6, A7, TARSKI:def_4; ::_thesis: verum end; then bool (union (rng B)) c= bool (union (rng the Sorts of U0)) by ZFMISC_1:67; then A8: bool (union (rng B)) c= bool (Union the Sorts of U0) by CARD_3:def_4; thus ( B in SubSort U0 implies B is opers_closed ) by Def11; ::_thesis: ( B is opers_closed implies B in SubSort U0 ) assume B is opers_closed ; ::_thesis: B in SubSort U0 then A9: for C being MSSubset of U0 st C = B holds C is opers_closed ; rng B c= bool (union (rng B)) by ZFMISC_1:82; then rng B c= bool (Union the Sorts of U0) by A8, XBOOLE_1:1; then B in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by A1, FUNCT_2:def_2; hence B in SubSort U0 by A9, Def11; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; let s be SortSymbol of S; func SubSort (A,s) -> set means :Def13: :: MSUALG_2:def 13 for x being set holds ( x in it iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) proof defpred S1[ set ] means ex B being MSSubset of U0 st ( B in SubSort A & \$1 = B . s ); set C = bool (Union the Sorts of U0); consider X being set such that A1: for x being set holds ( x in X iff ( x in bool (Union the Sorts of U0) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) A2: bool (Union the Sorts of U0) = bool (union (rng the Sorts of U0)) by CARD_3:def_4; for x being set holds ( x in X iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) proof dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2; then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def_3; then A3: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:74; let x be set ; ::_thesis: ( x in X iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) thus ( x in X implies ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) implies x in X ) given B being MSSubset of U0 such that A4: B in SubSort A and A5: x = B . s ; ::_thesis: x in X B c= the Sorts of U0 by PBOOLE:def_18; then B . s c= the Sorts of U0 . s by PBOOLE:def_2; then x c= union (rng the Sorts of U0) by A5, A3, XBOOLE_1:1; hence x in X by A1, A2, A4, A5; ::_thesis: verum end; hence for x being set holds ( x in X iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) ) & ( for x being set holds ( x in b2 iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex B being MSSubset of U0 st ( B in SubSort A & \$1 = B . s ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) ) & ( for x being set holds ( x in b2 iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def13 defines SubSort MSUALG_2:def_13_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 for s being SortSymbol of S for b5 being set holds ( b5 = SubSort (A,s) iff for x being set holds ( x in b5 iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) ); registration let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; let s be SortSymbol of S; cluster SubSort (A,s) -> non empty ; coherence not SubSort (A,s) is empty proof reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; defpred S1[ set ] means ex B being MSSubset of U0 st ( B in SubSort A & S = B . s ); set C = bool (Union the Sorts of U0); consider X being set such that A1: for x being set holds ( x in X iff ( x in bool (Union the Sorts of U0) & S1[x] ) ) from XBOOLE_0:sch_1(); A2: bool (Union the Sorts of U0) = bool (union (rng the Sorts of U0)) by CARD_3:def_4; A3: for x being set holds ( x in X iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) proof dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2; then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def_3; then A4: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:74; let x be set ; ::_thesis: ( x in X iff ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) thus ( x in X implies ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being MSSubset of U0 st ( B in SubSort A & x = B . s ) implies x in X ) given B being MSSubset of U0 such that A5: B in SubSort A and A6: x = B . s ; ::_thesis: x in X B c= the Sorts of U0 by PBOOLE:def_18; then B . s c= the Sorts of U0 . s by PBOOLE:def_2; then x c= union (rng the Sorts of U0) by A6, A4, XBOOLE_1:1; hence x in X by A1, A2, A5, A6; ::_thesis: verum end; A7: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def_18; u0 is opers_closed by Th3; then u0 in SubSort A by A7, Th13; then the Sorts of U0 . s in X by A3; then reconsider X = X as non empty set ; X = SubSort (A,s) by A3, Def13; hence not SubSort (A,s) is empty ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; func MSSubSort A -> MSSubset of U0 means :Def14: :: MSUALG_2:def 14 for s being SortSymbol of S holds it . s = meet (SubSort (A,s)); existence ex b1 being MSSubset of U0 st for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s)) proof deffunc H1( SortSymbol of S) -> set = meet (SubSort (A,\$1)); consider f being Function such that A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H1(s) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; f c= the Sorts of U0 proof reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S or f . x c= the Sorts of U0 . x ) A2: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def_18; assume x in the carrier of S ; ::_thesis: f . x c= the Sorts of U0 . x then reconsider s = x as SortSymbol of S ; u0 is opers_closed by Th3; then u0 in SubSort A by A2, Th13; then A3: the Sorts of U0 . s in SubSort (A,s) by Def13; f . s = meet (SubSort (A,s)) by A1; hence f . x c= the Sorts of U0 . x by A3, SETFAM_1:3; ::_thesis: verum end; then reconsider f = f as MSSubset of U0 by PBOOLE:def_18; take f ; ::_thesis: for s being SortSymbol of S holds f . s = meet (SubSort (A,s)) thus for s being SortSymbol of S holds f . s = meet (SubSort (A,s)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds b2 . s = meet (SubSort (A,s)) ) holds b1 = b2 proof let W1, W2 be MSSubset of U0; ::_thesis: ( ( for s being SortSymbol of S holds W1 . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds W2 . s = meet (SubSort (A,s)) ) implies W1 = W2 ) assume that A4: for s being SortSymbol of S holds W1 . s = meet (SubSort (A,s)) and A5: for s being SortSymbol of S holds W2 . s = meet (SubSort (A,s)) ; ::_thesis: W1 = W2 for s being set st s in the carrier of S holds W1 . s = W2 . s proof let s be set ; ::_thesis: ( s in the carrier of S implies W1 . s = W2 . s ) assume s in the carrier of S ; ::_thesis: W1 . s = W2 . s then reconsider s = s as SortSymbol of S ; W1 . s = meet (SubSort (A,s)) by A4; hence W1 . s = W2 . s by A5; ::_thesis: verum end; hence W1 = W2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def14 defines MSSubSort MSUALG_2:def_14_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A, b4 being MSSubset of U0 holds ( b4 = MSSubSort A iff for s being SortSymbol of S holds b4 . s = meet (SubSort (A,s)) ); theorem Th15: :: MSUALG_2:15 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A let A be MSSubset of U0; ::_thesis: (Constants U0) \/ A c= MSSubSort A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or ((Constants U0) \/ A) . i c= (MSSubSort A) . i ) assume i in the carrier of S ; ::_thesis: ((Constants U0) \/ A) . i c= (MSSubSort A) . i then reconsider s = i as SortSymbol of S ; A1: for Z being set st Z in SubSort (A,s) holds ((Constants U0) \/ A) . s c= Z proof let Z be set ; ::_thesis: ( Z in SubSort (A,s) implies ((Constants U0) \/ A) . s c= Z ) assume Z in SubSort (A,s) ; ::_thesis: ((Constants U0) \/ A) . s c= Z then consider B being MSSubset of U0 such that A2: B in SubSort A and A3: Z = B . s by Def13; ( Constants U0 c= B & A c= B ) by A2, Th13; then (Constants U0) \/ A c= B by PBOOLE:16; hence ((Constants U0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum end; (MSSubSort A) . s = meet (SubSort (A,s)) by Def14; hence ((Constants U0) \/ A) . i c= (MSSubSort A) . i by A1, SETFAM_1:5; ::_thesis: verum end; theorem Th16: :: MSUALG_2:16 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds MSSubSort A is V8() proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds MSSubSort A is V8() let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds MSSubSort A is V8() let A be MSSubset of U0; ::_thesis: ( (Constants U0) \/ A is V8() implies MSSubSort A is V8() ) assume A1: (Constants U0) \/ A is V8() ; ::_thesis: MSSubSort A is V8() now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ not_(MSSubSort_A)_._i_is_empty let i be set ; ::_thesis: ( i in the carrier of S implies not (MSSubSort A) . i is empty ) assume i in the carrier of S ; ::_thesis: not (MSSubSort A) . i is empty then reconsider s = i as SortSymbol of S ; for Z being set st Z in SubSort (A,s) holds ((Constants U0) \/ A) . s c= Z proof let Z be set ; ::_thesis: ( Z in SubSort (A,s) implies ((Constants U0) \/ A) . s c= Z ) assume Z in SubSort (A,s) ; ::_thesis: ((Constants U0) \/ A) . s c= Z then consider B being MSSubset of U0 such that A2: B in SubSort A and A3: Z = B . s by Def13; ( Constants U0 c= B & A c= B ) by A2, Th13; then (Constants U0) \/ A c= B by PBOOLE:16; hence ((Constants U0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum end; then A4: ((Constants U0) \/ A) . s c= meet (SubSort (A,s)) by SETFAM_1:5; ex x being set st x in ((Constants U0) \/ A) . s by A1, XBOOLE_0:def_1; hence not (MSSubSort A) . i is empty by A4, Def14; ::_thesis: verum end; hence MSSubSort A is V8() by PBOOLE:def_13; ::_thesis: verum end; theorem Th17: :: MSUALG_2:17 for S being non empty non void ManySortedSign for o being OperSymbol of S for U0 being MSAlgebra over S for A, B being MSSubset of U0 st B in SubSort A holds (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U0 being MSAlgebra over S for A, B being MSSubset of U0 st B in SubSort A holds (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o let o be OperSymbol of S; ::_thesis: for U0 being MSAlgebra over S for A, B being MSSubset of U0 st B in SubSort A holds (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o let U0 be MSAlgebra over S; ::_thesis: for A, B being MSSubset of U0 st B in SubSort A holds (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o let A, B be MSSubset of U0; ::_thesis: ( B in SubSort A implies (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o ) assume A1: B in SubSort A ; ::_thesis: (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o MSSubSort A c= B proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (MSSubSort A) . i c= B . i ) assume i in the carrier of S ; ::_thesis: (MSSubSort A) . i c= B . i then reconsider s = i as SortSymbol of S ; ( (MSSubSort A) . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, Def13, Def14; hence (MSSubSort A) . i c= B . i by SETFAM_1:3; ::_thesis: verum end; hence (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o by Th2; ::_thesis: verum end; theorem Th18: :: MSUALG_2:18 for S being non empty non void ManySortedSign for o being OperSymbol of S for U0 being MSAlgebra over S for A, B being MSSubset of U0 st B in SubSort A holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U0 being MSAlgebra over S for A, B being MSSubset of U0 st B in SubSort A holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o let o be OperSymbol of S; ::_thesis: for U0 being MSAlgebra over S for A, B being MSSubset of U0 st B in SubSort A holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o let U0 be MSAlgebra over S; ::_thesis: for A, B being MSSubset of U0 st B in SubSort A holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o let A, B be MSSubset of U0; ::_thesis: ( B in SubSort A implies rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o ) set m = (((MSSubSort A) #) * the Arity of S) . o; set b = ((B #) * the Arity of S) . o; set d = Den (o,U0); assume A1: B in SubSort A ; ::_thesis: rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o then (((B #) * the Arity of S) . o) /\ ((((MSSubSort A) #) * the Arity of S) . o) = (((MSSubSort A) #) * the Arity of S) . o by Th17, XBOOLE_1:28; then (Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o) = ((Den (o,U0)) | (((B #) * the Arity of S) . o)) | ((((MSSubSort A) #) * the Arity of S) . o) by RELAT_1:71; then A2: rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) by RELAT_1:70; B is opers_closed by A1, Th13; then B is_closed_on o by Def6; then rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by Def5; hence rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A2, XBOOLE_1:1; ::_thesis: verum end; theorem Th19: :: MSUALG_2:19 for S being non empty non void ManySortedSign for o being OperSymbol of S for U0 being MSAlgebra over S for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U0 being MSAlgebra over S for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o let o be OperSymbol of S; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o let A be MSSubset of U0; ::_thesis: rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) or x in ((MSSubSort A) * the ResultSort of S) . o ) assume that A1: x in rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) and A2: not x in ((MSSubSort A) * the ResultSort of S) . o ; ::_thesis: contradiction set r = the_result_sort_of o; A3: ( the_result_sort_of o = the ResultSort of S . o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_2; then ((MSSubSort A) * the ResultSort of S) . o = (MSSubSort A) . (the_result_sort_of o) by FUNCT_1:13 .= meet (SubSort (A,(the_result_sort_of o))) by Def14 ; then consider X being set such that A4: X in SubSort (A,(the_result_sort_of o)) and A5: not x in X by A2, SETFAM_1:def_1; consider B being MSSubset of U0 such that A6: B in SubSort A and A7: B . (the_result_sort_of o) = X by A4, Def13; rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A6, Th18; then x in (B * the ResultSort of S) . o by A1; hence contradiction by A3, A5, A7, FUNCT_1:13; ::_thesis: verum end; theorem Th20: :: MSUALG_2:20 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds ( MSSubSort A is opers_closed & A c= MSSubSort A ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 holds ( MSSubSort A is opers_closed & A c= MSSubSort A ) let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds ( MSSubSort A is opers_closed & A c= MSSubSort A ) let A be MSSubset of U0; ::_thesis: ( MSSubSort A is opers_closed & A c= MSSubSort A ) thus MSSubSort A is opers_closed ::_thesis: A c= MSSubSort A proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: MSSubSort A is_closed_on o rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o by Th19; hence MSSubSort A is_closed_on o by Def5; ::_thesis: verum end; ( A c= (Constants U0) \/ A & (Constants U0) \/ A c= MSSubSort A ) by Th15, PBOOLE:14; hence A c= MSSubSort A by PBOOLE:13; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; assume A1: A is opers_closed ; funcU0 | A -> strict MSSubAlgebra of U0 equals :Def15: :: MSUALG_2:def 15 MSAlgebra(# A,(Opers (U0,A)) #); coherence MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0 proof reconsider E = MSAlgebra(# A,(Opers (U0,A)) #) as MSAlgebra over S ; for B being MSSubset of U0 st B = the Sorts of E holds ( B is opers_closed & the Charact of E = Opers (U0,B) ) by A1; hence MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0 by Def9; ::_thesis: verum end; end; :: deftheorem Def15 defines | MSUALG_2:def_15_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 st A is opers_closed holds U0 | A = MSAlgebra(# A,(Opers (U0,A)) #); definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let U1, U2 be MSSubAlgebra of U0; funcU1 /\ U2 -> strict MSSubAlgebra of U0 means :Def16: :: MSUALG_2:def 16 ( the Sorts of it = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of it holds ( B is opers_closed & the Charact of it = Opers (U0,B) ) ) ); existence ex b1 being strict MSSubAlgebra of U0 st ( the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds ( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) ) proof the Sorts of U2 is MSSubset of U0 by Def9; then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by Def9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 /\ the Sorts of U2 c= the Sorts of U0 /\ the Sorts of U0 by A1, PBOOLE:21; then reconsider A = the Sorts of U1 /\ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; reconsider E = U0 | A as strict MSSubAlgebra of U0 ; take E ; ::_thesis: ( the Sorts of E = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of E holds ( B is opers_closed & the Charact of E = Opers (U0,B) ) ) ) A is opers_closed proof reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9; let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: A is_closed_on o A2: dom ((u1 #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2; A3: dom ((u2 #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2; u2 is opers_closed by Def9; then u2 is_closed_on o by Def6; then A4: rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by Def5; dom ((A #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2; then A5: ((A #) * the Arity of S) . o = (A #) . ( the Arity of S . o) by FUNCT_1:12 .= (A #) . (the_arity_of o) by MSUALG_1:def_1 .= product ((u1 /\ u2) * (the_arity_of o)) by FINSEQ_2:def_5 .= (product (u1 * (the_arity_of o))) /\ (product (u2 * (the_arity_of o))) by Th1 .= ((u1 #) . (the_arity_of o)) /\ (product (u2 * (the_arity_of o))) by FINSEQ_2:def_5 .= ((u1 #) . (the_arity_of o)) /\ ((u2 #) . (the_arity_of o)) by FINSEQ_2:def_5 .= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . (the_arity_of o)) by MSUALG_1:def_1 .= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . ( the Arity of S . o)) by MSUALG_1:def_1 .= (((u1 #) * the Arity of S) . o) /\ ((u2 #) . ( the Arity of S . o)) by A2, FUNCT_1:12 .= (((u1 #) * the Arity of S) . o) /\ (((u2 #) * the Arity of S) . o) by A3, FUNCT_1:12 ; then (Den (o,U0)) | (((A #) * the Arity of S) . o) = ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) | (((u1 #) * the Arity of S) . o) by RELAT_1:71; then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) by RELAT_1:70; then A6: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by A4, XBOOLE_1:1; u1 is opers_closed by Def9; then u1 is_closed_on o by Def6; then A7: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by Def5; A8: dom (u2 * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2; (Den (o,U0)) | (((A #) * the Arity of S) . o) = ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) | (((u2 #) * the Arity of S) . o) by A5, RELAT_1:71; then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) by RELAT_1:70; then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by A7, XBOOLE_1:1; then A9: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) by A6, XBOOLE_1:19; A10: dom (A * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2; dom (u1 * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2; then ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) = (u1 . ( the ResultSort of S . o)) /\ ((u2 * the ResultSort of S) . o) by FUNCT_1:12 .= (u1 . ( the ResultSort of S . o)) /\ (u2 . ( the ResultSort of S . o)) by A8, FUNCT_1:12 .= (u1 . (the_result_sort_of o)) /\ (u2 . ( the ResultSort of S . o)) by MSUALG_1:def_2 .= (u1 . (the_result_sort_of o)) /\ (u2 . (the_result_sort_of o)) by MSUALG_1:def_2 .= A . (the_result_sort_of o) by PBOOLE:def_5 .= A . ( the ResultSort of S . o) by MSUALG_1:def_2 .= (A * the ResultSort of S) . o by A10, FUNCT_1:12 ; hence A is_closed_on o by A9, Def5; ::_thesis: verum end; then U0 | A = MSAlgebra(# A,(Opers (U0,A)) #) by Def15; hence the Sorts of E = the Sorts of U1 /\ the Sorts of U2 ; ::_thesis: for B being MSSubset of U0 st B = the Sorts of E holds ( B is opers_closed & the Charact of E = Opers (U0,B) ) thus for B being MSSubset of U0 st B = the Sorts of E holds ( B is opers_closed & the Charact of E = Opers (U0,B) ) by Def9; ::_thesis: verum end; uniqueness for b1, b2 being strict MSSubAlgebra of U0 st the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds ( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) & the Sorts of b2 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b2 holds ( B is opers_closed & the Charact of b2 = Opers (U0,B) ) ) holds b1 = b2 by Th9; end; :: deftheorem Def16 defines /\ MSUALG_2:def_16_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 for b5 being strict MSSubAlgebra of U0 holds ( b5 = U1 /\ U2 iff ( the Sorts of b5 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b5 holds ( B is opers_closed & the Charact of b5 = Opers (U0,B) ) ) ) ); definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let A be MSSubset of U0; func GenMSAlg A -> strict MSSubAlgebra of U0 means :Def17: :: MSUALG_2:def 17 ( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds it is MSSubAlgebra of U1 ) ); existence ex b1 being strict MSSubAlgebra of U0 st ( A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds b1 is MSSubAlgebra of U1 ) ) proof set a = MSSubSort A; reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ; take u1 ; ::_thesis: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds u1 is MSSubAlgebra of U1 ) ) A1: u1 = MSAlgebra(# (MSSubSort A),(Opers (U0,(MSSubSort A))) #) by Def15, Th20; A c= MSSubSort A by Th20; hence A is MSSubset of u1 by A1, PBOOLE:def_18; ::_thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds u1 is MSSubAlgebra of U1 let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 ) reconsider B = the Sorts of U2 as MSSubset of U0 by Def9; assume A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2 then A2: A c= B by PBOOLE:def_18; Constants U0 is MSSubset of U2 by Th10; then A3: Constants U0 c= B by PBOOLE:def_18; B is opers_closed by Def9; then A4: B in SubSort A by A2, A3, Th13; the Sorts of u1 c= the Sorts of U2 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i ) assume i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i then reconsider s = i as SortSymbol of S ; ( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, A4, Def13, Def14; hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum end; hence u1 is MSSubAlgebra of U2 by Th8; ::_thesis: verum end; uniqueness for b1, b2 being strict MSSubAlgebra of U0 st A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds b1 is MSSubAlgebra of U1 ) & A is MSSubset of b2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds b2 is MSSubAlgebra of U1 ) holds b1 = b2 proof let W1, W2 be strict MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of W1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds W1 is MSSubAlgebra of U1 ) & A is MSSubset of W2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds W2 is MSSubAlgebra of U1 ) implies W1 = W2 ) assume ( A is MSSubset of W1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds W1 is MSSubAlgebra of U1 ) & A is MSSubset of W2 & ( for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds W2 is MSSubAlgebra of U2 ) ) ; ::_thesis: W1 = W2 then ( W1 is strict MSSubAlgebra of W2 & W2 is strict MSSubAlgebra of W1 ) ; hence W1 = W2 by Th7; ::_thesis: verum end; end; :: deftheorem Def17 defines GenMSAlg MSUALG_2:def_17_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 for b4 being strict MSSubAlgebra of U0 holds ( b4 = GenMSAlg A iff ( A is MSSubset of b4 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds b4 is MSSubAlgebra of U1 ) ) ); registration let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; let A be V8() MSSubset of U0; cluster GenMSAlg A -> strict non-empty ; coherence GenMSAlg A is non-empty proof (Constants U0) \/ A is V8() ; then reconsider a = MSSubSort A as V8() MSSubset of U0 by Th16; U0 | a = MSAlgebra(# a,(Opers (U0,a)) #) by Def15, Th20; then reconsider u1 = U0 | a as strict non-empty MSSubAlgebra of U0 by MSUALG_1:def_3; A1: A c= a by Th20; now__::_thesis:_(_A_is_MSSubset_of_u1_&_(_for_U2_being_MSSubAlgebra_of_U0_st_A_is_MSSubset_of_U2_holds_ u1_is_MSSubAlgebra_of_U2_)_) A2: u1 = MSAlgebra(# a,(Opers (U0,a)) #) by Def15, Th20; hence A is MSSubset of u1 by A1, PBOOLE:def_18; ::_thesis: for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds u1 is MSSubAlgebra of U2 let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 ) reconsider B = the Sorts of U2 as MSSubset of U0 by Def9; assume A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2 then A3: A c= B by PBOOLE:def_18; Constants U0 is MSSubset of U2 by Th10; then A4: Constants U0 c= B by PBOOLE:def_18; B is opers_closed by Def9; then A5: B in SubSort A by A3, A4, Th13; the Sorts of u1 c= the Sorts of U2 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i ) assume i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i then reconsider s = i as SortSymbol of S ; ( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A2, A5, Def13, Def14; hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum end; hence u1 is MSSubAlgebra of U2 by Th8; ::_thesis: verum end; hence GenMSAlg A is non-empty by Def17; ::_thesis: verum end; end; theorem Th21: :: MSUALG_2:21 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) ) set W = GenMSAlg B; reconsider B1 = the Sorts of (GenMSAlg B) as MSSubset of U0 by Def9; A1: the Charact of (GenMSAlg B) = Opers (U0,B1) by Def9; assume B = the Sorts of U0 ; ::_thesis: GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) then the Sorts of U0 is MSSubset of (GenMSAlg B) by Def17; then A2: the Sorts of U0 c= the Sorts of (GenMSAlg B) by PBOOLE:def_18; the Sorts of (GenMSAlg B) is MSSubset of U0 by Def9; then the Sorts of (GenMSAlg B) c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U0 = the Sorts of (GenMSAlg B) by A2, PBOOLE:146; hence GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) by A1, Th4; ::_thesis: verum end; theorem Th22: :: MSUALG_2:22 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for U1 being MSSubAlgebra of U0 for B being MSSubset of U0 st B = the Sorts of U1 holds GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for U1 being MSSubAlgebra of U0 for B being MSSubset of U0 st B = the Sorts of U1 holds GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) let U0 be MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 for B being MSSubset of U0 st B = the Sorts of U1 holds GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) let U1 be MSSubAlgebra of U0; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U1 holds GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) ) assume A1: B = the Sorts of U1 ; ::_thesis: GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) set W = GenMSAlg B; B is MSSubset of (GenMSAlg B) by Def17; then the Sorts of U1 c= the Sorts of (GenMSAlg B) by A1, PBOOLE:def_18; then A2: U1 is MSSubAlgebra of GenMSAlg B by Th8; B is MSSubset of U1 by A1, PBOOLE:def_18; then GenMSAlg B is MSSubAlgebra of U1 by Def17; hence GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) by A2, Th7; ::_thesis: verum end; theorem Th23: :: MSUALG_2:23 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) let U0 be non-empty MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) let U1 be MSSubAlgebra of U0; ::_thesis: (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) set C = Constants U0; set G = GenMSAlg (Constants U0); Constants U0 is MSSubset of U1 by Th10; then GenMSAlg (Constants U0) is strict MSSubAlgebra of U1 by Def17; then the Sorts of (GenMSAlg (Constants U0)) is MSSubset of U1 by Def9; then A1: the Sorts of (GenMSAlg (Constants U0)) c= the Sorts of U1 by PBOOLE:def_18; the Sorts of ((GenMSAlg (Constants U0)) /\ U1) = the Sorts of (GenMSAlg (Constants U0)) /\ the Sorts of U1 by Def16; then the Sorts of ((GenMSAlg (Constants U0)) /\ U1) = the Sorts of (GenMSAlg (Constants U0)) by A1, PBOOLE:23; hence (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) by Th9; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; let U1, U2 be MSSubAlgebra of U0; funcU1 "\/" U2 -> strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18 for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds it = GenMSAlg A; existence ex b1 being strict MSSubAlgebra of U0 st for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b1 = GenMSAlg A proof set B = the Sorts of U1 \/ the Sorts of U2; the Sorts of U2 is MSSubset of U0 by Def9; then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by Def9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16; then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; take GenMSAlg B ; ::_thesis: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds GenMSAlg B = GenMSAlg A thus for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds GenMSAlg B = GenMSAlg A ; ::_thesis: verum end; uniqueness for b1, b2 being strict MSSubAlgebra of U0 st ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b2 = GenMSAlg A ) holds b1 = b2 proof set B = the Sorts of U1 \/ the Sorts of U2; the Sorts of U2 is MSSubset of U0 by Def9; then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by Def9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16; then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; let W1, W2 be strict MSSubAlgebra of U0; ::_thesis: ( ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W2 = GenMSAlg A ) implies W1 = W2 ) assume that A3: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W1 = GenMSAlg A and A4: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W2 = GenMSAlg A ; ::_thesis: W1 = W2 W1 = GenMSAlg B by A3; hence W1 = W2 by A4; ::_thesis: verum end; end; :: deftheorem Def18 defines "\/" MSUALG_2:def_18_:_ for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 for b5 being strict MSSubAlgebra of U0 holds ( b5 = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b5 = GenMSAlg A ); theorem Th24: :: MSUALG_2:24 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1 being MSSubAlgebra of U0 for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds (GenMSAlg A) "\/" U1 = GenMSAlg B proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1 being MSSubAlgebra of U0 for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds (GenMSAlg A) "\/" U1 = GenMSAlg B let U0 be non-empty MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds (GenMSAlg A) "\/" U1 = GenMSAlg B let U1 be MSSubAlgebra of U0; ::_thesis: for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds (GenMSAlg A) "\/" U1 = GenMSAlg B let A, B be MSSubset of U0; ::_thesis: ( B = A \/ the Sorts of U1 implies (GenMSAlg A) "\/" U1 = GenMSAlg B ) reconsider u1 = the Sorts of U1, a = the Sorts of (GenMSAlg A) as MSSubset of U0 by Def9; A1: the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) c= a by PBOOLE:15; A2: the Sorts of ((GenMSAlg A) /\ (GenMSAlg B)) = the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by Def16; ( a c= the Sorts of U0 & u1 c= the Sorts of U0 ) by PBOOLE:def_18; then a \/ u1 c= the Sorts of U0 by PBOOLE:16; then reconsider b = a \/ u1 as MSSubset of U0 by PBOOLE:def_18; A3: (GenMSAlg A) "\/" U1 = GenMSAlg b by Def18; then a \/ u1 is MSSubset of ((GenMSAlg A) "\/" U1) by Def17; then A4: a \/ u1 c= the Sorts of ((GenMSAlg A) "\/" U1) by PBOOLE:def_18; A is MSSubset of (GenMSAlg A) by Def17; then A5: A c= the Sorts of (GenMSAlg A) by PBOOLE:def_18; B is MSSubset of (GenMSAlg B) by Def17; then A6: B c= the Sorts of (GenMSAlg B) by PBOOLE:def_18; assume A7: B = A \/ the Sorts of U1 ; ::_thesis: (GenMSAlg A) "\/" U1 = GenMSAlg B then A c= B by PBOOLE:14; then A c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13; then A c= the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by A5, PBOOLE:17; then A is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by A2, PBOOLE:def_18; then GenMSAlg A is MSSubAlgebra of (GenMSAlg A) /\ (GenMSAlg B) by Def17; then a is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by Def9; then a c= the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by A2, PBOOLE:def_18; then a = the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by A1, PBOOLE:146; then A8: a c= the Sorts of (GenMSAlg B) by PBOOLE:15; u1 c= B by A7, PBOOLE:14; then u1 c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13; then b c= the Sorts of (GenMSAlg B) by A8, PBOOLE:16; then b is MSSubset of (GenMSAlg B) by PBOOLE:def_18; then A9: GenMSAlg b is strict MSSubAlgebra of GenMSAlg B by Def17; A \/ u1 c= a \/ u1 by A5, PBOOLE:20; then B c= the Sorts of ((GenMSAlg A) "\/" U1) by A7, A4, PBOOLE:13; then B is MSSubset of ((GenMSAlg A) "\/" U1) by PBOOLE:def_18; then GenMSAlg B is strict MSSubAlgebra of (GenMSAlg A) "\/" U1 by Def17; hence (GenMSAlg A) "\/" U1 = GenMSAlg B by A3, A9, Th7; ::_thesis: verum end; theorem Th25: :: MSUALG_2:25 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1 being MSSubAlgebra of U0 for B being MSSubset of U0 st B = the Sorts of U0 holds (GenMSAlg B) "\/" U1 = GenMSAlg B proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1 being MSSubAlgebra of U0 for B being MSSubset of U0 st B = the Sorts of U0 holds (GenMSAlg B) "\/" U1 = GenMSAlg B let U0 be non-empty MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 for B being MSSubset of U0 st B = the Sorts of U0 holds (GenMSAlg B) "\/" U1 = GenMSAlg B let U1 be MSSubAlgebra of U0; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds (GenMSAlg B) "\/" U1 = GenMSAlg B let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies (GenMSAlg B) "\/" U1 = GenMSAlg B ) assume A1: B = the Sorts of U0 ; ::_thesis: (GenMSAlg B) "\/" U1 = GenMSAlg B the Sorts of U1 is MSSubset of U0 by Def9; then the Sorts of U1 c= B by A1, PBOOLE:def_18; then B \/ the Sorts of U1 = B by PBOOLE:22; hence (GenMSAlg B) "\/" U1 = GenMSAlg B by Th24; ::_thesis: verum end; theorem Th26: :: MSUALG_2:26 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1 let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1 let U1, U2 be MSSubAlgebra of U0; ::_thesis: U1 "\/" U2 = U2 "\/" U1 reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9; ( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18; then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16; then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18; U1 "\/" U2 = GenMSAlg A by Def18; hence U1 "\/" U2 = U2 "\/" U1 by Def18; ::_thesis: verum end; theorem Th27: :: MSUALG_2:27 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) let U1, U2 be MSSubAlgebra of U0; ::_thesis: U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9; A1: the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 /\ the Sorts of (U1 "\/" U2) by Def16; ( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18; then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16; then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18; U1 "\/" U2 = GenMSAlg A by Def18; then A is MSSubset of (U1 "\/" U2) by Def17; then A2: A c= the Sorts of (U1 "\/" U2) by PBOOLE:def_18; the Sorts of U1 c= A by PBOOLE:14; then the Sorts of U1 c= the Sorts of (U1 "\/" U2) by A2, PBOOLE:13; then A3: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/" U2)) by A1, PBOOLE:17; reconsider u112 = the Sorts of (U1 /\ (U1 "\/" U2)) as MSSubset of U0 by Def9; A4: the Charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112) by Def16; the Sorts of (U1 /\ (U1 "\/" U2)) c= the Sorts of U1 by A1, PBOOLE:15; then the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 by A3, PBOOLE:146; hence U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) by A4, Def9; ::_thesis: verum end; theorem Th28: :: MSUALG_2:28 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) let U1, U2 be MSSubAlgebra of U0; ::_thesis: (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by Def9; ( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18; then u12 \/ u2 c= the Sorts of U0 by PBOOLE:16; then reconsider A = u12 \/ u2 as MSSubset of U0 by PBOOLE:def_18; u12 = the Sorts of U1 /\ the Sorts of U2 by Def16; then u12 c= u2 by PBOOLE:15; then A1: A = u2 by PBOOLE:22; (U1 /\ U2) "\/" U2 = GenMSAlg A by Def18; hence (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, Th22; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; func MSSub U0 -> set means :Def19: :: MSUALG_2:def 19 for x being set holds ( x in it iff x is strict MSSubAlgebra of U0 ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict MSSubAlgebra of U0 ) proof reconsider X = { (GenMSAlg (@ A)) where A is Element of SubSort U0 : verum } as set ; take X ; ::_thesis: for x being set holds ( x in X iff x is strict MSSubAlgebra of U0 ) let x be set ; ::_thesis: ( x in X iff x is strict MSSubAlgebra of U0 ) thus ( x in X implies x is strict MSSubAlgebra of U0 ) ::_thesis: ( x is strict MSSubAlgebra of U0 implies x in X ) proof assume x in X ; ::_thesis: x is strict MSSubAlgebra of U0 then ex A being Element of SubSort U0 st x = GenMSAlg (@ A) ; hence x is strict MSSubAlgebra of U0 ; ::_thesis: verum end; assume x is strict MSSubAlgebra of U0 ; ::_thesis: x in X then reconsider a = x as strict MSSubAlgebra of U0 ; reconsider A = the Sorts of a as MSSubset of U0 by Def9; A is opers_closed by Def9; then reconsider h = A as Element of SubSort U0 by Th14; a = GenMSAlg (@ h) by Th22; hence x in X ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict MSSubAlgebra of U0 ) ) & ( for x being set holds ( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds b1 = b2 proof defpred S1[ set ] means \$1 is strict MSSubAlgebra of U0; for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict MSSubAlgebra of U0 ) ) & ( for x being set holds ( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def19 defines MSSub MSUALG_2:def_19_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for b3 being set holds ( b3 = MSSub U0 iff for x being set holds ( x in b3 iff x is strict MSSubAlgebra of U0 ) ); registration let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; cluster MSSub U0 -> non empty ; coherence not MSSub U0 is empty proof set x = the strict MSSubAlgebra of U0; the strict MSSubAlgebra of U0 in MSSub U0 by Def19; hence not MSSub U0 is empty ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; func MSAlg_join U0 -> BinOp of (MSSub U0) means :Def20: :: MSUALG_2:def 20 for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds it . (x,y) = U1 "\/" U2; existence ex b1 being BinOp of (MSSub U0) st for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 "\/" U2 proof defpred S1[ Element of MSSub U0, Element of MSSub U0, Element of MSSub U0] means for U1, U2 being strict MSSubAlgebra of U0 st \$1 = U1 & \$2 = U2 holds \$3 = U1 "\/" U2; A1: for x, y being Element of MSSub U0 ex z being Element of MSSub U0 st S1[x,y,z] proof let x, y be Element of MSSub U0; ::_thesis: ex z being Element of MSSub U0 st S1[x,y,z] reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; reconsider z = U1 "\/" U2 as Element of MSSub U0 by Def19; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] ; ::_thesis: verum end; consider o being BinOp of (MSSub U0) such that A2: for a, b being Element of MSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take o ; ::_thesis: for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 "\/" U2 thus for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 "\/" U2 by A2; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 "\/" U2 ) holds b1 = b2 proof let o1, o2 be BinOp of (MSSub U0); ::_thesis: ( ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 "\/" U2 ) implies o1 = o2 ) assume that A3: for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 "\/" U2 and A4: for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 "\/" U2 ; ::_thesis: o1 = o2 for x, y being Element of MSSub U0 holds o1 . (x,y) = o2 . (x,y) proof let x, y be Element of MSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y) reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; o1 . (x,y) = U1 "\/" U2 by A3; hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def20 defines MSAlg_join MSUALG_2:def_20_:_ for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for b3 being BinOp of (MSSub U0) holds ( b3 = MSAlg_join U0 iff for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b3 . (x,y) = U1 "\/" U2 ); definition let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; func MSAlg_meet U0 -> BinOp of (MSSub U0) means :Def21: :: MSUALG_2:def 21 for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds it . (x,y) = U1 /\ U2; existence ex b1 being BinOp of (MSSub U0) st for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 /\ U2 proof defpred S1[ Element of MSSub U0, Element of MSSub U0, Element of MSSub U0] means for U1, U2 being strict MSSubAlgebra of U0 st \$1 = U1 & \$2 = U2 holds \$3 = U1 /\ U2; A1: for x, y being Element of MSSub U0 ex z being Element of MSSub U0 st S1[x,y,z] proof let x, y be Element of MSSub U0; ::_thesis: ex z being Element of MSSub U0 st S1[x,y,z] reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; reconsider z = U1 /\ U2 as Element of MSSub U0 by Def19; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] ; ::_thesis: verum end; consider o being BinOp of (MSSub U0) such that A2: for a, b being Element of MSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take o ; ::_thesis: for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 /\ U2 thus for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 /\ U2 by A2; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 /\ U2 ) holds b1 = b2 proof let o1, o2 be BinOp of (MSSub U0); ::_thesis: ( ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 /\ U2 ) implies o1 = o2 ) assume that A3: for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 /\ U2 and A4: for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 /\ U2 ; ::_thesis: o1 = o2 for x, y being Element of MSSub U0 holds o1 . (x,y) = o2 . (x,y) proof let x, y be Element of MSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y) reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; o1 . (x,y) = U1 /\ U2 by A3; hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def21 defines MSAlg_meet MSUALG_2:def_21_:_ for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for b3 being BinOp of (MSSub U0) holds ( b3 = MSAlg_meet U0 iff for x, y being Element of MSSub U0 for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds b3 . (x,y) = U1 /\ U2 ); theorem Th29: :: MSUALG_2:29 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_join U0 is commutative set o = MSAlg_join U0; for x, y being Element of MSSub U0 holds (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x) proof let x, y be Element of MSSub U0; ::_thesis: (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x) reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; set B = the Sorts of U1 \/ the Sorts of U2; the Sorts of U2 is MSSubset of U0 by Def9; then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by Def9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16; then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; A2: U1 "\/" U2 = GenMSAlg B by Def18; ( (MSAlg_join U0) . (x,y) = U1 "\/" U2 & (MSAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def20; hence (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x) by A2, Def18; ::_thesis: verum end; hence MSAlg_join U0 is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th30: :: MSUALG_2:30 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_join U0 is associative set o = MSAlg_join U0; for x, y, z being Element of MSSub U0 holds (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z) proof let x, y, z be Element of MSSub U0; ::_thesis: (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z) reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19; set B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3); A1: (MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20; the Sorts of U2 is MSSubset of U0 by Def9; then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U3 is MSSubset of U0 by Def9; then the Sorts of U3 c= the Sorts of U0 by PBOOLE:def_18; then A3: the Sorts of U2 \/ the Sorts of U3 c= the Sorts of U0 by A2, PBOOLE:16; then reconsider C = the Sorts of U2 \/ the Sorts of U3 as MSSubset of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by Def9; then A4: the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then A5: the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) c= the Sorts of U0 by A3, PBOOLE:16; the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A4, A2, PBOOLE:16; then reconsider D = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; reconsider B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) as MSSubset of U0 by A5, PBOOLE:def_18; A6: B = D \/ the Sorts of U3 by PBOOLE:28; A7: (U1 "\/" U2) "\/" U3 = (GenMSAlg D) "\/" U3 by Def18 .= GenMSAlg B by A6, Th24 ; (MSAlg_join U0) . (y,z) = U2 "\/" U3 by Def20; then A8: (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = U1 "\/" (U2 "\/" U3) by Def20; U1 "\/" (U2 "\/" U3) = U1 "\/" (GenMSAlg C) by Def18 .= (GenMSAlg C) "\/" U1 by Th26 .= GenMSAlg B by Th24 ; hence (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z) by A1, A8, A7, Def20; ::_thesis: verum end; hence MSAlg_join U0 is associative by BINOP_1:def_3; ::_thesis: verum end; theorem Th31: :: MSUALG_2:31 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_meet U0 is commutative set o = MSAlg_meet U0; for x, y being Element of MSSub U0 holds (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x) proof let x, y be Element of MSSub U0; ::_thesis: (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x) reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; A1: ( the Sorts of (U2 /\ U1) = the Sorts of U2 /\ the Sorts of U1 & ( for B2 being MSSubset of U0 st B2 = the Sorts of (U2 /\ U1) holds ( B2 is opers_closed & the Charact of (U2 /\ U1) = Opers (U0,B2) ) ) ) by Def16; ( (MSAlg_meet U0) . (x,y) = U1 /\ U2 & (MSAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def21; hence (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x) by A1, Def16; ::_thesis: verum end; hence MSAlg_meet U0 is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th32: :: MSUALG_2:32 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_meet U0 is associative set o = MSAlg_meet U0; for x, y, z being Element of MSSub U0 holds (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) proof let x, y, z be Element of MSSub U0; ::_thesis: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19; reconsider u23 = U2 /\ U3, u12 = U1 /\ U2 as Element of MSSub U0 by Def19; A1: ( the Sorts of (U1 /\ U2) = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of (U1 /\ (U2 /\ U3)) holds ( B is opers_closed & the Charact of (U1 /\ (U2 /\ U3)) = Opers (U0,B) ) ) ) by Def16; A2: (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) = (MSAlg_meet U0) . (u12,z) by Def21 .= (U1 /\ U2) /\ U3 by Def21 ; the Sorts of (U2 /\ U3) = the Sorts of U2 /\ the Sorts of U3 by Def16; then A3: the Sorts of (U1 /\ (U2 /\ U3)) = the Sorts of U1 /\ ( the Sorts of U2 /\ the Sorts of U3) by Def16; then reconsider C = the Sorts of U1 /\ ( the Sorts of U2 /\ the Sorts of U3) as MSSubset of U0 by Def9; A4: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (x,u23) by Def21 .= U1 /\ (U2 /\ U3) by Def21 ; C = ( the Sorts of U1 /\ the Sorts of U2) /\ the Sorts of U3 by PBOOLE:29; hence (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A4, A2, A3, A1, Def16; ::_thesis: verum end; hence MSAlg_meet U0 is associative by BINOP_1:def_3; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; func MSSubAlLattice U0 -> strict Lattice equals :: MSUALG_2:def 22 LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); coherence LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice proof set L = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); A1: for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c MSAlg_join U0 is associative by Th30; hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by BINOP_1:def_3; ::_thesis: verum end; A2: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" b = b "/\" a proof let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "/\" b = b "/\" a MSAlg_meet U0 is commutative by Th31; hence a "/\" b = b "/\" a by BINOP_1:def_2; ::_thesis: verum end; A3: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (a "\/" b) = a proof let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "/\" (a "\/" b) = a reconsider x = a, y = b as Element of MSSub U0 ; (MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = x proof reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; (MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20; hence (MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/" U2) by Def21 .= x by Th27 ; ::_thesis: verum end; hence a "/\" (a "\/" b) = a ; ::_thesis: verum end; A4: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds (a "/\" b) "\/" b = b proof let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: (a "/\" b) "\/" b = b reconsider x = a, y = b as Element of MSSub U0 ; (MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = y proof reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19; (MSAlg_meet U0) . (x,y) = U1 /\ U2 by Def21; hence (MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def20 .= y by Th28 ; ::_thesis: verum end; hence (a "/\" b) "\/" b = b ; ::_thesis: verum end; A5: for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c MSAlg_meet U0 is associative by Th32; hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by BINOP_1:def_3; ::_thesis: verum end; for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" b = b "\/" a proof let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "\/" b = b "\/" a MSAlg_join U0 is commutative by Th29; hence a "\/" b = b "\/" a by BINOP_1:def_2; ::_thesis: verum end; then ( LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-absorbing & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice ; ::_thesis: verum end; end; :: deftheorem defines MSSubAlLattice MSUALG_2:def_22_:_ for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); theorem Th33: :: MSUALG_2:33 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded let U0 be non-empty MSAlgebra over S; ::_thesis: MSSubAlLattice U0 is bounded set L = MSSubAlLattice U0; thus MSSubAlLattice U0 is lower-bounded :: according to LATTICES:def_15 ::_thesis: MSSubAlLattice U0 is upper-bounded proof set C = Constants U0; reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19; reconsider G1 = G as Element of (MSSubAlLattice U0) ; take G1 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (MSSubAlLattice U0) holds ( G1 "/\" b1 = G1 & b1 "/\" G1 = G1 ) let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 ) reconsider a1 = a as Element of MSSub U0 ; reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19; thus G1 "/\" a = (GenMSAlg (Constants U0)) /\ a2 by Def21 .= G1 by Th23 ; ::_thesis: a "/\" G1 = G1 hence a "/\" G1 = G1 ; ::_thesis: verum end; thus MSSubAlLattice U0 is upper-bounded ::_thesis: verum proof reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; reconsider G = GenMSAlg B as Element of MSSub U0 by Def19; reconsider G1 = G as Element of (MSSubAlLattice U0) ; take G1 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (MSSubAlLattice U0) holds ( G1 "\/" b1 = G1 & b1 "\/" G1 = G1 ) let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 ) reconsider a1 = a as Element of MSSub U0 ; reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19; thus G1 "\/" a = (GenMSAlg B) "\/" a2 by Def20 .= G1 by Th25 ; ::_thesis: a "\/" G1 = G1 hence a "\/" G1 = G1 ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let U0 be non-empty MSAlgebra over S; cluster MSSubAlLattice U0 -> strict bounded ; coherence MSSubAlLattice U0 is bounded by Th33; end; theorem :: MSUALG_2:34 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0) let U0 be non-empty MSAlgebra over S; ::_thesis: Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0) set C = Constants U0; reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19; set L = MSSubAlLattice U0; reconsider G1 = G as Element of (MSSubAlLattice U0) ; now__::_thesis:_for_a_being_Element_of_(MSSubAlLattice_U0)_holds_ (_G1_"/\"_a_=_G1_&_a_"/\"_G1_=_G1_) let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 ) reconsider a1 = a as Element of MSSub U0 ; reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19; thus G1 "/\" a = (GenMSAlg (Constants U0)) /\ a2 by Def21 .= G1 by Th23 ; ::_thesis: a "/\" G1 = G1 hence a "/\" G1 = G1 ; ::_thesis: verum end; hence Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0) by LATTICES:def_16; ::_thesis: verum end; theorem Th35: :: MSUALG_2:35 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds Top (MSSubAlLattice U0) = GenMSAlg B proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for B being MSSubset of U0 st B = the Sorts of U0 holds Top (MSSubAlLattice U0) = GenMSAlg B let U0 be non-empty MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds Top (MSSubAlLattice U0) = GenMSAlg B let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Top (MSSubAlLattice U0) = GenMSAlg B ) reconsider G = GenMSAlg B as Element of MSSub U0 by Def19; set L = MSSubAlLattice U0; reconsider G1 = G as Element of (MSSubAlLattice U0) ; assume A1: B = the Sorts of U0 ; ::_thesis: Top (MSSubAlLattice U0) = GenMSAlg B now__::_thesis:_for_a_being_Element_of_(MSSubAlLattice_U0)_holds_ (_G1_"\/"_a_=_G1_&_a_"\/"_G1_=_G1_) let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 ) reconsider a1 = a as Element of MSSub U0 ; reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19; thus G1 "\/" a = (GenMSAlg B) "\/" a2 by Def20 .= G1 by A1, Th25 ; ::_thesis: a "\/" G1 = G1 hence a "\/" G1 = G1 ; ::_thesis: verum end; hence Top (MSSubAlLattice U0) = GenMSAlg B by LATTICES:def_17; ::_thesis: verum end; theorem :: MSUALG_2:36 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #) let U0 be non-empty MSAlgebra over S; ::_thesis: Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #) reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; thus Top (MSSubAlLattice U0) = GenMSAlg B by Th35 .= MSAlgebra(# the Sorts of U0, the Charact of U0 #) by Th21 ; ::_thesis: verum end; theorem :: MSUALG_2:37 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1; theorem :: MSUALG_2:38 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds the Sorts of U0 in SubSort A by Lm2; theorem :: MSUALG_2:39 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds SubSort A c= SubSort U0 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 holds SubSort A c= SubSort U0 let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds SubSort A c= SubSort U0 let A be MSSubset of U0; ::_thesis: SubSort A c= SubSort U0 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort A or x in SubSort U0 ) assume A1: x in SubSort A ; ::_thesis: x in SubSort U0 A2: for B being MSSubset of U0 st B = x holds B is opers_closed by A1, Def10; ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 ) by A1, Def10; hence x in SubSort U0 by A2, Def11; ::_thesis: verum end;