:: MSSUBLAT semantic presentation begin theorem Th1: :: MSSUBLAT:1 for a being set holds (*--> a) . 0 = {} proof let a be set ; ::_thesis: (*--> a) . 0 = {} thus (*--> a) . 0 = 0 |-> a by FINSEQ_2:def_6 .= {} ; ::_thesis: verum end; theorem :: MSSUBLAT:2 for a being set holds (*--> a) . 1 = <*a*> proof let a be set ; ::_thesis: (*--> a) . 1 = <*a*> thus (*--> a) . 1 = 1 |-> a by FINSEQ_2:def_6 .= <*a*> by FINSEQ_2:59 ; ::_thesis: verum end; theorem :: MSSUBLAT:3 for a being set holds (*--> a) . 2 = <*a,a*> proof let a be set ; ::_thesis: (*--> a) . 2 = <*a,a*> thus (*--> a) . 2 = 2 |-> a by FINSEQ_2:def_6 .= <*a,a*> by FINSEQ_2:61 ; ::_thesis: verum end; theorem :: MSSUBLAT:4 for a being set holds (*--> a) . 3 = <*a,a,a*> proof let a be set ; ::_thesis: (*--> a) . 3 = <*a,a,a*> thus (*--> a) . 3 = 3 |-> a by FINSEQ_2:def_6 .= <*a,a,a*> by FINSEQ_2:62 ; ::_thesis: verum end; theorem Th5: :: MSSUBLAT:5 for i being Nat for f being FinSequence of {0} holds ( f = i |-> 0 iff len f = i ) proof let i be Nat; ::_thesis: for f being FinSequence of {0} holds ( f = i |-> 0 iff len f = i ) let f be FinSequence of {0}; ::_thesis: ( f = i |-> 0 iff len f = i ) thus ( f = i |-> 0 implies len f = i ) by CARD_1:def_7; ::_thesis: ( len f = i implies f = i |-> 0 ) assume len f = i ; ::_thesis: f = i |-> 0 then A1: dom f = Seg i by FINSEQ_1:def_3; percases ( Seg i = {} or Seg i <> {} ) ; supposeA2: Seg i = {} ; ::_thesis: f = i |-> 0 hence f = {} by A1 .= 0 |-> 0 .= i |-> 0 by A2 ; ::_thesis: verum end; supposeA3: Seg i <> {} ; ::_thesis: f = i |-> 0 rng f c= {0} by FINSEQ_1:def_4; then ( rng f = {0} or rng f = {} ) by ZFMISC_1:33; hence f = i |-> 0 by A1, A3, FUNCOP_1:9, RELAT_1:42; ::_thesis: verum end; end; end; theorem Th6: :: MSSUBLAT:6 for i being Nat for f being FinSequence st f = (*--> 0) . i holds len f = i proof let i be Nat; ::_thesis: for f being FinSequence st f = (*--> 0) . i holds len f = i let p be FinSequence; ::_thesis: ( p = (*--> 0) . i implies len p = i ) assume A1: p = (*--> 0) . i ; ::_thesis: len p = i i in NAT by ORDINAL1:def_12; then p = i |-> 0 by A1, FINSEQ_2:def_6; hence len p = i by CARD_1:def_7; ::_thesis: verum end; begin reconsider z = 0 as Element of {0} by TARSKI:def_1; theorem Th7: :: MSSUBLAT:7 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds MSSign U1 = MSSign U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies MSSign U1 = MSSign U2 ) set ff2 = (dom (signature U1)) --> z; set gg2 = (dom (signature U2)) --> z; reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; assume U1 is SubAlgebra of U2 ; ::_thesis: MSSign U1 = MSSign U2 then A1: U1,U2 are_similar by UNIALG_2:13; A2: ( MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) & MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) ) by MSUALG_1:10; then the carrier' of (MSSign U1) = the carrier' of (MSSign U2) by A1, UNIALG_2:def_1; hence MSSign U1 = MSSign U2 by A1, A2, UNIALG_2:def_1; ::_thesis: verum end; theorem Th8: :: MSSUBLAT:8 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds for o being OperSymbol of (MSSign U2) for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds for o being OperSymbol of (MSSign U2) for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) ) assume A1: U1 is SubAlgebra of U2 ; ::_thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds for o being OperSymbol of (MSSign U2) for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) A2: MSSign U1 = MSSign U2 by A1, Th7; A3: MSSign U1 = MSSign U2 by A1, Th7; let B be MSSubset of (MSAlg U2); ::_thesis: ( B = the Sorts of (MSAlg U1) implies for o being OperSymbol of (MSSign U2) for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) ) assume A4: B = the Sorts of (MSAlg U1) ; ::_thesis: for o being OperSymbol of (MSSign U2) for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) let o be OperSymbol of (MSSign U2); ::_thesis: for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) reconsider a = o as Element of the carrier' of (MSSign U1) by A1, Th7; set X = Args (a,(MSAlg U1)); set Y = dom (Den (a,(MSAlg U1))); ( the Sorts of (MSAlg U2) is MSSubset of (MSAlg U2) & B c= the Sorts of (MSAlg U2) ) by PBOOLE:def_18; then A5: ((B #) * the Arity of (MSSign U1)) . a c= (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . o by A3, MSUALG_2:2; ( dom (Den (o,(MSAlg U2))) = Args (o,(MSAlg U2)) & Args (o,(MSAlg U2)) = (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . o ) by FUNCT_2:def_1, MSUALG_1:def_4; then Args (a,(MSAlg U1)) c= dom (Den (o,(MSAlg U2))) by A4, A2, A5, MSUALG_1:def_4; then dom ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) = Args (a,(MSAlg U1)) by RELAT_1:62; then dom ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) = dom (Den (a,(MSAlg U1))) by FUNCT_2:def_1; then A6: dom (Den (a,(MSAlg U1))) = (dom (Den (o,(MSAlg U2)))) /\ (Args (a,(MSAlg U1))) by RELAT_1:61; for x being set st x in dom (Den (a,(MSAlg U1))) holds (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x proof MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; then the Sorts of (MSAlg U1) = 0 .--> the carrier of U1 by MSUALG_1:def_9; then rng the Sorts of (MSAlg U1) = { the carrier of U1} by FUNCOP_1:8; then A7: the carrier of U1 is Component of the Sorts of (MSAlg U1) by TARSKI:def_1; reconsider cc = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def_7; let x be set ; ::_thesis: ( x in dom (Den (a,(MSAlg U1))) implies (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x ) A8: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; U1,U2 are_similar by A1, UNIALG_2:13; then A9: signature U1 = signature U2 by UNIALG_2:def_1; assume x in dom (Den (a,(MSAlg U1))) ; ::_thesis: (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x then x in Args (a,(MSAlg U1)) by A6, XBOOLE_0:def_4; then x in (len (the_arity_of a)) -tuples_on (the_sort_of (MSAlg U1)) by MSUALG_1:6; then A10: x in (len (the_arity_of a)) -tuples_on the carrier of U1 by A7, MSUALG_1:def_12; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; set ff1 = (*--> 0) * (signature U1); set ff2 = (dom (signature U1)) --> z; set gg2 = (dom (signature U2)) --> z; reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2; consider n being Nat such that A11: dom (signature U2) = Seg n by FINSEQ_1:def_2; A12: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10; then A13: a in Seg n by A11; A14: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3 .= Seg (len (signature U2)) by UNIALG_1:def_4 .= dom (signature U2) by FINSEQ_1:def_3 ; then reconsider op = the charact of U2 . a as operation of U2 by A12, FUNCT_1:def_3; reconsider a = a as Element of NAT by A13; A15: rng (signature U1) c= NAT by FINSEQ_1:def_4; U1,U2 are_similar by A1, UNIALG_2:13; then A16: signature U1 = signature U2 by UNIALG_2:def_1; then A17: (signature U1) . a in rng (signature U1) by A12, FUNCT_1:def_3; then reconsider sig = (signature U1) . a as Element of NAT by A15; dom (*--> 0) = NAT by FUNCT_2:def_1; then ( MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) & a in dom ((*--> 0) * (signature U1)) ) by A12, A16, A17, A15, FUNCT_1:11, MSUALG_1:10; then the Arity of (MSSign U1) . a = (*--> 0) . ((signature U1) . a) by FUNCT_1:12; then A18: the Arity of (MSSign U1) . a = sig |-> 0 by FINSEQ_2:def_6; reconsider ar = the Arity of (MSSign U1) . a as FinSequence ; x in (len ar) -tuples_on the carrier of U1 by A10, MSUALG_1:def_1; then x in sig -tuples_on the carrier of U1 by A18, CARD_1:def_7; then A19: x in (arity op) -tuples_on the carrier of U1 by A12, A9, UNIALG_1:def_4; now__::_thesis:_for_n_being_set_st_n_in_dom_(Opers_(U2,cc))_holds_ (Opers_(U2,cc))_._n_is_Function let n be set ; ::_thesis: ( n in dom (Opers (U2,cc)) implies (Opers (U2,cc)) . n is Function ) assume n in dom (Opers (U2,cc)) ; ::_thesis: (Opers (U2,cc)) . n is Function then ( rng (Opers (U2,cc)) c= PFuncs ((cc *),cc) & (Opers (U2,cc)) . n in rng (Opers (U2,cc)) ) by FINSEQ_1:def_4, FUNCT_1:def_3; hence (Opers (U2,cc)) . n is Function by PARTFUN1:46; ::_thesis: verum end; then reconsider f = Opers (U2,cc) as Function-yielding Function by FUNCOP_1:def_6; cc is opers_closed by A1, UNIALG_2:def_7; then A20: cc is_closed_on op by UNIALG_2:def_4; a in dom the charact of U2 by A12, A14; then A21: o in dom (Opers (U2,cc)) by UNIALG_2:def_6; reconsider a = a as OperSymbol of (MSSign U1) ; MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; then (Den (a,(MSAlg U1))) . x = ((MSCharact U1) . o) . x by MSUALG_1:def_6 .= ( the charact of U1 . o) . x by MSUALG_1:def_10 .= (f . o) . x by A1, UNIALG_2:def_7 .= (op /. cc) . x by A21, UNIALG_2:def_6 .= (op | ((arity op) -tuples_on cc)) . x by A20, UNIALG_2:def_5 .= ( the charact of U2 . o) . x by A19, FUNCT_1:49 .= ( the Charact of (MSAlg U2) . o) . x by A8, MSUALG_1:def_10 .= (Den (o,(MSAlg U2))) . x by MSUALG_1:def_6 ; hence (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x ; ::_thesis: verum end; hence for a being OperSymbol of (MSSign U1) st a = o holds Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) by A6, FUNCT_1:46; ::_thesis: verum end; theorem Th9: :: MSSUBLAT:9 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) ) set gg1 = (*--> 0) * (signature U2); set gg2 = (dom (signature U2)) --> z; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; A1: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10; MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; then A2: the Sorts of (MSAlg U2) = 0 .--> the carrier of U2 by MSUALG_1:def_9; assume A3: U1 is SubAlgebra of U2 ; ::_thesis: the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) then MSSign U1 = MSSign U2 by Th7; then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2 ; MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; then A4: the Sorts of A = 0 .--> the carrier of U1 by MSUALG_1:def_9; A5: 0 in {0} by TARSKI:def_1; A6: the carrier of U1 is Subset of U2 by A3, UNIALG_2:def_7; the Sorts of A c= the Sorts of (MSAlg U2) proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of (MSSign U2) or the Sorts of A . i c= the Sorts of (MSAlg U2) . i ) assume i in the carrier of (MSSign U2) ; ::_thesis: the Sorts of A . i c= the Sorts of (MSAlg U2) . i then A7: i = 0 by A1, TARSKI:def_1; ( the Sorts of A . 0 = the carrier of U1 & the Sorts of (MSAlg U2) . 0 = the carrier of U2 ) by A4, A2, A5, FUNCOP_1:7; hence the Sorts of A . i c= the Sorts of (MSAlg U2) . i by A6, A7; ::_thesis: verum end; hence the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) by PBOOLE:def_18; ::_thesis: verum end; theorem Th10: :: MSSUBLAT:10 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds B is opers_closed proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds B is opers_closed ) assume A1: U1 is SubAlgebra of U2 ; ::_thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds B is opers_closed let B be MSSubset of (MSAlg U2); ::_thesis: ( B = the Sorts of (MSAlg U1) implies B is opers_closed ) assume A2: B = the Sorts of (MSAlg U1) ; ::_thesis: B is opers_closed let o be OperSymbol of (MSSign U2); :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o reconsider a = o as Element of the carrier' of (MSSign U1) by A1, Th7; set S = (B * the ResultSort of (MSSign U2)) . a; (B * the ResultSort of (MSSign U2)) . a = ( the Sorts of (MSAlg U1) * the ResultSort of (MSSign U1)) . a by A1, A2, Th7; then A3: (B * the ResultSort of (MSSign U2)) . a = Result (a,(MSAlg U1)) by MSUALG_1:def_5; set Z = rng ((Den (o,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . a)); MSSign U1 = MSSign U2 by A1, Th7; then ( rng (Den (a,(MSAlg U1))) c= Result (a,(MSAlg U1)) & rng ((Den (o,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . a)) = rng ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) ) by A2, MSUALG_1:def_4, RELAT_1:def_19; then rng ((Den (o,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . a)) c= Result (a,(MSAlg U1)) by A1, A2, Th8; hence B is_closed_on o by A3, MSUALG_2:def_5; ::_thesis: verum end; theorem Th11: :: MSSUBLAT:11 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) ) assume A1: U1 is SubAlgebra of U2 ; ::_thesis: for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) let B be MSSubset of (MSAlg U2); ::_thesis: ( B = the Sorts of (MSAlg U1) implies the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) ) set f1 = the Charact of (MSAlg U1); set f2 = Opers ((MSAlg U2),B); the carrier' of (MSSign U1) = the carrier' of (MSSign U2) proof set ff1 = (*--> 0) * (signature U1); set ff2 = (dom (signature U1)) --> z; set gg1 = (*--> 0) * (signature U2); set gg2 = (dom (signature U2)) --> z; reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; A2: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10; ( U1,U2 are_similar & MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) ) by A1, MSUALG_1:10, UNIALG_2:13; hence the carrier' of (MSSign U1) = the carrier' of (MSSign U2) by A2, UNIALG_2:def_1; ::_thesis: verum end; then reconsider f1 = the Charact of (MSAlg U1) as ManySortedSet of the carrier' of (MSSign U2) ; assume A3: B = the Sorts of (MSAlg U1) ; ::_thesis: the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) for x being set st x in the carrier' of (MSSign U2) holds f1 . x = (Opers ((MSAlg U2),B)) . x proof let x be set ; ::_thesis: ( x in the carrier' of (MSSign U2) implies f1 . x = (Opers ((MSAlg U2),B)) . x ) assume A4: x in the carrier' of (MSSign U2) ; ::_thesis: f1 . x = (Opers ((MSAlg U2),B)) . x then reconsider y = x as OperSymbol of (MSSign U2) ; reconsider x = x as OperSymbol of (MSSign U1) by A1, A4, Th7; B is opers_closed by A1, A3, Th10; then ( (Opers ((MSAlg U2),B)) . y = y /. B & B is_closed_on y ) by MSUALG_2:def_6, MSUALG_2:def_8; then A5: (Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | (((B #) * the Arity of (MSSign U2)) . y) by MSUALG_2:def_7; ((B #) * the Arity of (MSSign U1)) . x = (( the Sorts of (MSAlg U1) #) * the Arity of (MSSign U1)) . x by A1, A3, Th7; then (Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | ((( the Sorts of (MSAlg U1) #) * the Arity of (MSSign U1)) . x) by A1, A5, Th7; then ( f1 . x = Den (x,(MSAlg U1)) & (Opers ((MSAlg U2),B)) . y = (Den (y,(MSAlg U2))) | (Args (x,(MSAlg U1))) ) by MSUALG_1:def_4, MSUALG_1:def_6; hence f1 . x = (Opers ((MSAlg U2),B)) . x by A1, A3, Th8; ::_thesis: verum end; hence the Charact of (MSAlg U1) = Opers ((MSAlg U2),B) by PBOOLE:3; ::_thesis: verum end; theorem Th12: :: MSSUBLAT:12 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds MSAlg U1 is MSSubAlgebra of MSAlg U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies MSAlg U1 is MSSubAlgebra of MSAlg U2 ) assume A1: U1 is SubAlgebra of U2 ; ::_thesis: MSAlg U1 is MSSubAlgebra of MSAlg U2 then MSSign U1 = MSSign U2 by Th7; then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2 ; A is MSSubAlgebra of MSAlg U2 proof thus the Sorts of A is MSSubset of (MSAlg U2) by A1, Th9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of (MSAlg U2) holds ( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers ((MSAlg U2),b1) ) ) let B be MSSubset of (MSAlg U2); ::_thesis: ( not B = the Sorts of A or ( B is opers_closed & the Charact of A = Opers ((MSAlg U2),B) ) ) assume A2: B = the Sorts of A ; ::_thesis: ( B is opers_closed & the Charact of A = Opers ((MSAlg U2),B) ) hence B is opers_closed by A1, Th10; ::_thesis: the Charact of A = Opers ((MSAlg U2),B) thus the Charact of A = Opers ((MSAlg U2),B) by A1, A2, Th11; ::_thesis: verum end; hence MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: verum end; theorem Th13: :: MSSUBLAT:13 for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds the carrier of U1 is Subset of U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies the carrier of U1 is Subset of U2 ) set MU1 = MSAlg U1; set MU2 = MSAlg U2; assume A1: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: the carrier of U1 is Subset of U2 then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ; reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A1, MSUALG_2:def_9; set gg1 = (*--> 0) * (signature U2); set gg2 = (dom (signature U2)) --> z; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; reconsider C1 = C as ManySortedSet of the carrier of (MSSign U2) ; A2: 0 in {0} by TARSKI:def_1; MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; then A3: C1 c= MSSorts U2 by PBOOLE:def_18; ( MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) & MSSorts U2 = 0 .--> the carrier of U2 ) by MSUALG_1:10, MSUALG_1:def_9; then ( MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) & C1 . 0 c= ({0} --> the carrier of U2) . 0 ) by A3, MSUALG_1:def_11, PBOOLE:def_2; then (MSSorts U1) . 0 c= the carrier of U2 by A2, FUNCOP_1:7; then (0 .--> the carrier of U1) . 0 c= the carrier of U2 by MSUALG_1:def_9; hence the carrier of U1 is Subset of U2 by A2, FUNCOP_1:7; ::_thesis: verum end; theorem Th14: :: MSSUBLAT:14 for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds for B being non empty Subset of U2 st B = the carrier of U1 holds B is opers_closed proof let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies for B being non empty Subset of U2 st B = the carrier of U1 holds B is opers_closed ) set MU1 = MSAlg U1; set MU2 = MSAlg U2; A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; assume A2: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds B is opers_closed then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ; let B be non empty Subset of U2; ::_thesis: ( B = the carrier of U1 implies B is opers_closed ) assume A3: B = the carrier of U1 ; ::_thesis: B is opers_closed let o be operation of U2; :: according to UNIALG_2:def_4 ::_thesis: B is_closed_on o reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def_9; A4: MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; set gg1 = (*--> 0) * (signature U2); set gg2 = (dom (signature U2)) --> z; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; A5: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10; A6: C is opers_closed by A2, MSUALG_2:def_9; thus B is_closed_on o ::_thesis: verum proof A7: 0 in {0} by TARSKI:def_1; let s be FinSequence of B; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in B ) consider n being set such that A8: n in dom the charact of U2 and A9: o = the charact of U2 . n by FUNCT_1:def_3; A10: ( dom the charact of U2 = Seg (len the charact of U2) & dom (signature U2) = Seg (len (signature U2)) ) by FINSEQ_1:def_3; then A11: n in dom (signature U2) by A8, UNIALG_1:def_4; reconsider n = n as OperSymbol of (MSSign U2) by A5, A8, A10, UNIALG_1:def_4; assume A12: len s = arity o ; ::_thesis: o . s in B ex y being set st ( y in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) & ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . y = o . s ) proof take s ; ::_thesis: ( s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) & ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = o . s ) thus s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) ::_thesis: ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = o . s proof (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) by A5, FINSEQ_2:63; then reconsider ao0 = (arity o) |-> 0 as Element of the carrier of (MSSign U2) * by FINSEQ_1:def_11; A13: now__::_thesis:_(_Seg_(arity_o)_=_{}_implies_(arity_o)_|->_0_is_FinSequence_of_the_carrier_of_(MSSign_U2)_) assume Seg (arity o) = {} ; ::_thesis: (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) then (arity o) |-> 0 = <*> the carrier of (MSSign U2) ; hence (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) ; ::_thesis: verum end; ( Seg (arity o) <> {} implies ( dom ((arity o) |-> 0) = Seg (arity o) & rng ((arity o) |-> 0) c= the carrier of (MSSign U2) ) ) by A5, FUNCOP_1:13; then (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) by A13, FINSEQ_1:def_4; then reconsider aro = (arity o) |-> 0 as Element of the carrier of (MSSign U2) * by FINSEQ_1:def_11; A14: dom the Arity of (MSSign U2) = the carrier' of (MSSign U2) by FUNCT_2:def_1; the Sorts of (MSAlg U2) = 0 .--> the carrier of U2 by A1, MSUALG_1:def_9; then A15: the Sorts of (MSAlg U2) * aro = (arity o) |-> the carrier of U2 by FINSEQ_2:144 .= (Seg (arity o)) --> the carrier of U2 ; dom s = Seg (arity o) by A12, FINSEQ_1:def_3; then A16: dom s = dom ( the Sorts of (MSAlg U2) * aro) by A15, FUNCT_2:def_1; A17: for x being set st x in dom ( the Sorts of (MSAlg U2) * aro) holds s . x in ( the Sorts of (MSAlg U2) * aro) . x proof let x be set ; ::_thesis: ( x in dom ( the Sorts of (MSAlg U2) * aro) implies s . x in ( the Sorts of (MSAlg U2) * aro) . x ) rng s c= B by FINSEQ_1:def_4; then A18: rng s c= the carrier of U2 by XBOOLE_1:1; assume A19: x in dom ( the Sorts of (MSAlg U2) * aro) ; ::_thesis: s . x in ( the Sorts of (MSAlg U2) * aro) . x s . x in rng s by A16, A19, FUNCT_1:def_3; then A20: ( 0 in {0} & s . x in the carrier of U2 ) by A18, TARSKI:def_1; ( the Sorts of (MSAlg U2) * aro) . x = the Sorts of (MSAlg U2) . (aro . x) by A19, FUNCT_1:12 .= (MSSorts U2) . 0 by A1 .= (0 .--> the carrier of U2) . 0 by MSUALG_1:def_9 ; hence s . x in ( the Sorts of (MSAlg U2) * aro) . x by A20, FUNCOP_1:7; ::_thesis: verum end; dom (Den (n,(MSAlg U2))) = Args (n,(MSAlg U2)) by FUNCT_2:def_1; then dom (Den (n,(MSAlg U2))) = (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . n by MSUALG_1:def_4 .= ( the Sorts of (MSAlg U2) #) . (((*--> 0) * (signature U2)) . n) by A5, A14, FUNCT_1:13 .= ( the Sorts of (MSAlg U2) #) . ((*--> 0) . ((signature U2) . n)) by A11, FUNCT_1:13 .= ( the Sorts of (MSAlg U2) #) . ((*--> 0) . (arity o)) by A9, A11, UNIALG_1:def_4 .= ( the Sorts of (MSAlg U2) #) . ((arity o) |-> 0) by FINSEQ_2:def_6 ; then dom (Den (n,(MSAlg U2))) = product ( the Sorts of (MSAlg U2) * aro) by FINSEQ_2:def_5; then A21: s in dom (Den (n,(MSAlg U2))) by A16, A17, CARD_3:def_5; A22: s is Element of (len s) -tuples_on B by FINSEQ_2:92; A23: 0 in {0} by TARSKI:def_1; A24: n in dom (signature U2) by A8, A10, UNIALG_1:def_4; A25: C = 0 .--> the carrier of U1 by A4, MSUALG_1:def_9; then dom C = {0} by FUNCOP_1:13; then A26: 0 in dom C by TARSKI:def_1; ( dom (*--> 0) = NAT & (signature U2) . n = arity o ) by A9, A11, FUNCT_2:def_1, UNIALG_1:def_4; then A27: n in dom ((*--> 0) * (signature U2)) by A24, FUNCT_1:11; then ((C #) * the Arity of (MSSign U2)) . n = (C #) . (((*--> 0) * (signature U2)) . n) by A5, FUNCT_1:13 .= (C #) . ((*--> 0) . ((signature U2) . n)) by A27, FUNCT_1:12 .= (C #) . ((*--> 0) . (arity o)) by A9, A24, UNIALG_1:def_4 .= (C #) . ((arity o) |-> 0) by FINSEQ_2:def_6 ; then ((C #) * the Arity of (MSSign U2)) . n = product (C * ao0) by FINSEQ_2:def_5 .= product ((Seg (arity o)) --> (C . 0)) by A26, FUNCOP_1:17 .= product ((Seg (arity o)) --> B) by A3, A25, A23, FUNCOP_1:7 .= Funcs ((Seg (arity o)),B) by CARD_3:11 .= (arity o) -tuples_on B by FINSEQ_2:93 ; then s in (dom (Den (n,(MSAlg U2)))) /\ (((C #) * the Arity of (MSSign U2)) . n) by A12, A21, A22, XBOOLE_0:def_4; hence s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) by RELAT_1:61; ::_thesis: verum end; hence ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = (Den (n,(MSAlg U2))) . s by FUNCT_1:47 .= ((MSCharact U2) . n) . s by A1, MSUALG_1:def_6 .= o . s by A9, MSUALG_1:def_10 ; ::_thesis: verum end; then A28: o . s in rng ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) by FUNCT_1:def_3; C is_closed_on n by A6, MSUALG_2:def_6; then A29: rng ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) c= (C * the ResultSort of (MSSign U2)) . n by MSUALG_2:def_5; n in dom ((dom (signature U2)) --> 0) by A11, FUNCOP_1:13; then (C * the ResultSort of (MSSign U2)) . n = C . (((dom (signature U2)) --> 0) . n) by A5, FUNCT_1:13 .= the Sorts of MU1 . 0 by A11, FUNCOP_1:7 .= (0 .--> the carrier of U1) . 0 by A4, MSUALG_1:def_9 .= B by A3, A7, FUNCOP_1:7 ; hence o . s in B by A29, A28; ::_thesis: verum end; end; theorem Th15: :: MSSUBLAT:15 for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds for B being non empty Subset of U2 st B = the carrier of U1 holds the charact of U1 = Opers (U2,B) proof let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies for B being non empty Subset of U2 st B = the carrier of U1 holds the charact of U1 = Opers (U2,B) ) set MU1 = MSAlg U1; set MU2 = MSAlg U2; A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; assume A2: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds the charact of U1 = Opers (U2,B) then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ; reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def_9; A3: the Charact of MU1 = Opers ((MSAlg U2),C) by A2, MSUALG_2:def_9; set gg1 = (*--> 0) * (signature U2); set gg2 = (dom (signature U2)) --> z; reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; A4: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10; let B be non empty Subset of U2; ::_thesis: ( B = the carrier of U1 implies the charact of U1 = Opers (U2,B) ) assume A5: B = the carrier of U1 ; ::_thesis: the charact of U1 = Opers (U2,B) then reconsider ch1 = the charact of U1 as PFuncFinSequence of B ; A6: MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; then A7: dom ch1 = dom the Charact of MU1 by MSUALG_1:def_10 .= the carrier' of (MSSign U2) by PARTFUN1:def_2 .= Seg (len (signature U2)) by A4, FINSEQ_1:def_3 .= Seg (len the charact of U2) by UNIALG_1:def_4 .= dom the charact of U2 by FINSEQ_1:def_3 ; A8: C is opers_closed by A2, MSUALG_2:def_9; for n being set for o being operation of U2 st n in dom ch1 & o = the charact of U2 . n holds ch1 . n = o /. B proof A9: C = 0 .--> the carrier of U1 by A6, MSUALG_1:def_9; then dom C = {0} by FUNCOP_1:13; then A10: 0 in dom C by TARSKI:def_1; let n be set ; ::_thesis: for o being operation of U2 st n in dom ch1 & o = the charact of U2 . n holds ch1 . n = o /. B let o be operation of U2; ::_thesis: ( n in dom ch1 & o = the charact of U2 . n implies ch1 . n = o /. B ) assume that A11: n in dom ch1 and A12: o = the charact of U2 . n ; ::_thesis: ch1 . n = o /. B n in dom the Charact of (MSAlg U2) by A1, A7, A11, MSUALG_1:def_10; then reconsider N = n as OperSymbol of (MSSign U2) by PARTFUN1:def_2; A13: ( dom the charact of U2 = Seg (len the charact of U2) & dom (signature U2) = Seg (len (signature U2)) ) by FINSEQ_1:def_3; then A14: N in dom (signature U2) by A7, A11, UNIALG_1:def_4; (arity o) |-> 0 is FinSequence of the carrier of (MSSign U2) by A4, FINSEQ_2:63; then reconsider ao0 = (arity o) |-> 0 as Element of the carrier of (MSSign U2) * by FINSEQ_1:def_11; A15: C is_closed_on N by A8, MSUALG_2:def_6; B is opers_closed by A2, A5, Th14; then A16: B is_closed_on o by UNIALG_2:def_4; A17: 0 in {0} by TARSKI:def_1; N in dom (signature U2) by A7, A11, A13, UNIALG_1:def_4; then ( dom (*--> 0) = NAT & (signature U2) . N = arity o ) by A12, FUNCT_2:def_1, UNIALG_1:def_4; then A18: N in dom ((*--> 0) * (signature U2)) by A14, FUNCT_1:11; then ((C #) * the Arity of (MSSign U2)) . N = (C #) . (((*--> 0) * (signature U2)) . N) by A4, FUNCT_1:13 .= (C #) . ((*--> 0) . ((signature U2) . N)) by A18, FUNCT_1:12 .= (C #) . ((*--> 0) . (arity o)) by A12, A14, UNIALG_1:def_4 .= (C #) . ((arity o) |-> 0) by FINSEQ_2:def_6 ; then A19: ((C #) * the Arity of (MSSign U2)) . N = product (C * ao0) by FINSEQ_2:def_5 .= product ((Seg (arity o)) --> (C . 0)) by A10, FUNCOP_1:17 .= product ((Seg (arity o)) --> B) by A5, A9, A17, FUNCOP_1:7 .= Funcs ((Seg (arity o)),B) by CARD_3:11 .= (arity o) -tuples_on B by FINSEQ_2:93 ; ch1 . N = the Charact of MU1 . N by A6, MSUALG_1:def_10 .= N /. C by A3, MSUALG_2:def_8 .= (Den (N,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . N) by A15, MSUALG_2:def_7 .= ((MSCharact U2) . N) | (((C #) * the Arity of (MSSign U2)) . N) by A1, MSUALG_1:def_6 .= o | ((arity o) -tuples_on B) by A12, A19, MSUALG_1:def_10 ; hence ch1 . n = o /. B by A16, UNIALG_2:def_5; ::_thesis: verum end; hence the charact of U1 = Opers (U2,B) by A7, UNIALG_2:def_6; ::_thesis: verum end; theorem Th16: :: MSSUBLAT:16 for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds U1 is SubAlgebra of U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies U1 is SubAlgebra of U2 ) assume A1: MSAlg U1 is MSSubAlgebra of MSAlg U2 ; ::_thesis: U1 is SubAlgebra of U2 hence the carrier of U1 is Subset of U2 by Th13; :: according to UNIALG_2:def_7 ::_thesis: for b1 being Element of K19( the carrier of U2) holds ( not b1 = the carrier of U1 or ( the charact of U1 = Opers (U2,b1) & b1 is opers_closed ) ) let B be non empty Subset of U2; ::_thesis: ( not B = the carrier of U1 or ( the charact of U1 = Opers (U2,B) & B is opers_closed ) ) assume B = the carrier of U1 ; ::_thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed ) hence ( the charact of U1 = Opers (U2,B) & B is opers_closed ) by A1, Th14, Th15; ::_thesis: verum end; theorem Th17: :: MSSUBLAT:17 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A) proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A) let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A) let B be non-empty MSSubAlgebra of A; ::_thesis: the carrier of (1-Alg B) is Subset of (1-Alg A) the Sorts of B is MSSubset of A by MSUALG_2:def_9; then A1: the Sorts of B c= the Sorts of A by PBOOLE:def_18; 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14; then reconsider c = the carrier of (1-Alg B) as Component of the Sorts of B by MSUALG_1:def_12; 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14; then reconsider d = the carrier of (1-Alg A) as Component of the Sorts of A by MSUALG_1:def_12; A2: dom the Sorts of A = the carrier of MS by PARTFUN1:def_2; then consider dr being set such that A3: dr in the carrier of MS and A4: d = the Sorts of A . dr by FUNCT_1:def_3; dom the Sorts of A = dom the Sorts of B by A2, PARTFUN1:def_2; then consider cr being set such that A5: cr in the carrier of MS and A6: c = the Sorts of B . cr by A2, FUNCT_1:def_3; cr = dr by A5, A3, STRUCT_0:def_10; hence the carrier of (1-Alg B) is Subset of (1-Alg A) by A1, A5, A6, A4, PBOOLE:def_2; ::_thesis: verum end; theorem Th18: :: MSSUBLAT:18 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds S is opers_closed proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds S is opers_closed let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds S is opers_closed let B be non-empty MSSubAlgebra of A; ::_thesis: for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds S is opers_closed reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def_9; A1: C is opers_closed by MSUALG_2:def_9; A2: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14; let S be non empty Subset of (1-Alg A); ::_thesis: ( S = the carrier of (1-Alg B) implies S is opers_closed ) assume A3: S = the carrier of (1-Alg B) ; ::_thesis: S is opers_closed set 1A = 1-Alg A; A4: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14; let o be operation of (1-Alg A); :: according to UNIALG_2:def_4 ::_thesis: S is_closed_on o A5: dom the Sorts of A = the carrier of MS by PARTFUN1:def_2; then A6: dom the Sorts of A = dom the Sorts of B by PARTFUN1:def_2; thus S is_closed_on o ::_thesis: verum proof reconsider com = S as Component of the Sorts of B by A2, A3, MSUALG_1:def_12; consider n being set such that A7: n in dom the charact of (1-Alg A) and A8: o = the charact of (1-Alg A) . n by FUNCT_1:def_3; n in dom the Charact of A by A4, A7, MSUALG_1:def_13; then reconsider n = n as OperSymbol of MS by PARTFUN1:def_2; reconsider crn = C . ( the ResultSort of MS . n) as Component of the Sorts of B by A5, A6, FUNCT_1:def_3; let s be FinSequence of S; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in S ) A9: dom the Arity of MS = the carrier' of MS by FUNCT_2:def_1; assume A10: len s = arity o ; ::_thesis: o . s in S ex y being set st ( y in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) & ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . y = o . s ) proof take s ; ::_thesis: ( s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) & ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = o . s ) A11: the Charact of A . n = the charact of (1-Alg A) . n by A4, MSUALG_1:def_13; thus s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) ::_thesis: ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = o . s proof rng s c= S by FINSEQ_1:def_4; then rng s c= the carrier of (1-Alg A) by XBOOLE_1:1; then reconsider s1 = s as FinSequence of the carrier of (1-Alg A) by FINSEQ_1:def_4; reconsider An = the Arity of MS . n as Element of the carrier of MS * ; set f = the Sorts of A * An; consider d being set such that A12: d in dom o by XBOOLE_0:def_1; o in PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) by PARTFUN1:45; then ex o1 being Function st ( o1 = o & dom o1 c= the carrier of (1-Alg A) * & rng o1 c= the carrier of (1-Alg A) ) by PARTFUN1:def_3; then reconsider d = d as FinSequence of the carrier of (1-Alg A) by A12, FINSEQ_1:def_11; A13: dom (Den (n,A)) = Args (n,A) by FUNCT_2:def_1 .= (len (the_arity_of n)) -tuples_on the carrier of (1-Alg A) by A4, MSUALG_1:6 ; dom (Den (n,A)) = Args (n,A) by FUNCT_2:def_1; then dom (Den (n,A)) = (( the Sorts of A #) * the Arity of MS) . n by MSUALG_1:def_4 .= ( the Sorts of A #) . ( the Arity of MS . n) by A9, FUNCT_1:13 ; then A14: dom (Den (n,A)) = product ( the Sorts of A * An) by FINSEQ_2:def_5; A15: o = the Charact of A . n by A4, A8, MSUALG_1:def_13 .= Den (n,A) by MSUALG_1:def_6 ; len d = len s1 by A10, A12, MARGREL1:def_25; then len s = len (the_arity_of n) by A12, A15, A13, CARD_1:def_7; then A16: dom s = Seg (len (the_arity_of n)) by FINSEQ_1:def_3 .= dom (the_arity_of n) by FINSEQ_1:def_3 .= dom An by MSUALG_1:def_1 ; A17: dom s c= dom (C * An) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom s or x in dom (C * An) ) assume A18: x in dom s ; ::_thesis: x in dom (C * An) then ( rng An c= the carrier of MS & An . x in rng An ) by A16, FINSEQ_1:def_4, FUNCT_1:def_3; then An . x in the carrier of MS ; then An . x in dom C by PARTFUN1:def_2; hence x in dom (C * An) by A16, A18, FUNCT_1:11; ::_thesis: verum end; dom (C * An) c= dom s by A16, RELAT_1:25; then A19: dom s = dom (C * An) by A17, XBOOLE_0:def_10; A20: for x being set st x in dom s holds s . x in (C * An) . x proof let x be set ; ::_thesis: ( x in dom s implies s . x in (C * An) . x ) A21: rng s c= S by FINSEQ_1:def_4; assume A22: x in dom s ; ::_thesis: s . x in (C * An) . x then A23: s . x in rng s by FUNCT_1:def_3; dom s c= dom An by A19, RELAT_1:25; then ( rng An c= the carrier of MS & An . x in rng An ) by A22, FINSEQ_1:def_4, FUNCT_1:def_3; then An . x in the carrier of MS ; then A24: An . x in dom C by PARTFUN1:def_2; (C * An) . x = C . (An . x) by A17, A22, FUNCT_1:12; then reconsider canx = (C * An) . x as Component of C by A24, FUNCT_1:def_3; (C * An) . x = canx .= S by A2, A3, MSUALG_1:def_12 ; hence s . x in (C * An) . x by A23, A21; ::_thesis: verum end; A25: dom ( the Sorts of A * An) c= dom s proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ( the Sorts of A * An) or x in dom s ) assume x in dom ( the Sorts of A * An) ; ::_thesis: x in dom s hence x in dom s by A16, FUNCT_1:11; ::_thesis: verum end; A26: for x being set st x in dom ( the Sorts of A * An) holds s . x in ( the Sorts of A * An) . x proof let x be set ; ::_thesis: ( x in dom ( the Sorts of A * An) implies s . x in ( the Sorts of A * An) . x ) A27: rng s c= S by FINSEQ_1:def_4; assume A28: x in dom ( the Sorts of A * An) ; ::_thesis: s . x in ( the Sorts of A * An) . x then ( the Sorts of A * An) . x in rng ( the Sorts of A * An) by FUNCT_1:def_3; then reconsider fx = ( the Sorts of A * An) . x as Component of the Sorts of A by FUNCT_1:14; s . x in rng s by A25, A28, FUNCT_1:def_3; then ( fx = the_sort_of A & s . x in S ) by A27, MSUALG_1:def_12; hence s . x in ( the Sorts of A * An) . x by A4; ::_thesis: verum end; dom the Arity of MS = the carrier' of MS by FUNCT_2:def_1; then ((C #) * the Arity of MS) . n = (C #) . An by FUNCT_1:13 .= product (C * An) by FINSEQ_2:def_5 ; then A29: s in ((C #) * the Arity of MS) . n by A19, A20, CARD_3:9; dom s c= dom ( the Sorts of A * An) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom s or x in dom ( the Sorts of A * An) ) assume A30: x in dom s ; ::_thesis: x in dom ( the Sorts of A * An) then ( rng An c= the carrier of MS & An . x in rng An ) by A16, FINSEQ_1:def_4, FUNCT_1:def_3; then An . x in the carrier of MS ; then An . x in dom the Sorts of A by PARTFUN1:def_2; hence x in dom ( the Sorts of A * An) by A16, A30, FUNCT_1:11; ::_thesis: verum end; then dom s = dom ( the Sorts of A * An) by A25, XBOOLE_0:def_10; then s in dom (Den (n,A)) by A14, A26, CARD_3:9; then s in (dom (Den (n,A))) /\ (((C #) * the Arity of MS) . n) by A29, XBOOLE_0:def_4; hence s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) by RELAT_1:61; ::_thesis: verum end; hence ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = (Den (n,A)) . s by FUNCT_1:47 .= o . s by A8, A11, MSUALG_1:def_6 ; ::_thesis: verum end; then A31: o . s in rng ((Den (n,A)) | (((C #) * the Arity of MS) . n)) by FUNCT_1:def_3; dom the ResultSort of MS = the carrier' of MS by FUNCT_2:def_1; then A32: (C * the ResultSort of MS) . n = crn by FUNCT_1:13 .= com by MSUALG_1:5 ; C is_closed_on n by A1, MSUALG_2:def_6; then rng ((Den (n,A)) | (((C #) * the Arity of MS) . n)) c= (C * the ResultSort of MS) . n by MSUALG_2:def_5; hence o . s in S by A31, A32; ::_thesis: verum end; end; theorem Th19: :: MSSUBLAT:19 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds the charact of (1-Alg B) = Opers ((1-Alg A),S) proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds the charact of (1-Alg B) = Opers ((1-Alg A),S) let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds the charact of (1-Alg B) = Opers ((1-Alg A),S) let B be non-empty MSSubAlgebra of A; ::_thesis: for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds the charact of (1-Alg B) = Opers ((1-Alg A),S) reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def_9; A1: the Charact of B = Opers (A,C) by MSUALG_2:def_9; set 1B = 1-Alg B; set 1A = 1-Alg A; A2: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14; set f1 = the charact of (1-Alg B); let S be non empty Subset of (1-Alg A); ::_thesis: ( S = the carrier of (1-Alg B) implies the charact of (1-Alg B) = Opers ((1-Alg A),S) ) assume A3: S = the carrier of (1-Alg B) ; ::_thesis: the charact of (1-Alg B) = Opers ((1-Alg A),S) reconsider f1 = the charact of (1-Alg B) as PFuncFinSequence of S by A3; A4: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14; then A5: f1 = the Charact of B by MSUALG_1:def_13; A6: C is opers_closed by MSUALG_2:def_9; A7: for n being set for o being operation of (1-Alg A) st n in dom f1 & o = the charact of (1-Alg A) . n holds f1 . n = o /. S proof let n be set ; ::_thesis: for o being operation of (1-Alg A) st n in dom f1 & o = the charact of (1-Alg A) . n holds f1 . n = o /. S let o be operation of (1-Alg A); ::_thesis: ( n in dom f1 & o = the charact of (1-Alg A) . n implies f1 . n = o /. S ) assume that A8: n in dom f1 and A9: o = the charact of (1-Alg A) . n ; ::_thesis: f1 . n = o /. S reconsider y = n as OperSymbol of MS by A5, A8, PARTFUN1:def_2; o = the Charact of A . y by A2, A9, MSUALG_1:def_13 .= Den (y,A) by MSUALG_1:def_6 ; then A10: dom o = Args (y,A) by FUNCT_2:def_1 .= (len (the_arity_of y)) -tuples_on (the_sort_of A) by MSUALG_1:6 ; now__::_thesis:_(_ex_x_being_FinSequence_st_x_in_dom_o_&_(_for_x_being_FinSequence_st_x_in_dom_o_holds_ len_(the_arity_of_y)_=_len_x_)_) set a = the Element of (len (the_arity_of y)) -tuples_on (the_sort_of A); the Element of (len (the_arity_of y)) -tuples_on (the_sort_of A) in dom o by A10; hence ex x being FinSequence st x in dom o ; ::_thesis: for x being FinSequence st x in dom o holds len (the_arity_of y) = len x let x be FinSequence; ::_thesis: ( x in dom o implies len (the_arity_of y) = len x ) assume x in dom o ; ::_thesis: len (the_arity_of y) = len x then ex s being Element of (the_sort_of A) * st ( x = s & len s = len (the_arity_of y) ) by A10; hence len (the_arity_of y) = len x ; ::_thesis: verum end; then A11: arity o = len (the_arity_of y) by MARGREL1:def_25; S is opers_closed by A3, Th18; then A12: S is_closed_on o by UNIALG_2:def_4; A13: C is_closed_on y by A6, MSUALG_2:def_6; A14: ((C #) * the Arity of MS) . y = Args (y,B) by MSUALG_1:def_4 .= (arity o) -tuples_on S by A4, A3, A11, MSUALG_1:6 ; f1 . n = the Charact of B . y by A4, MSUALG_1:def_13 .= y /. C by A1, MSUALG_2:def_8 .= (Den (y,A)) | (((C #) * the Arity of MS) . y) by A13, MSUALG_2:def_7 .= ( the Charact of A . y) | (((C #) * the Arity of MS) . y) by MSUALG_1:def_6 .= o | ((arity o) -tuples_on S) by A2, A9, A14, MSUALG_1:def_13 ; hence f1 . n = o /. S by A12, UNIALG_2:def_5; ::_thesis: verum end; dom f1 = the carrier' of MS by A5, PARTFUN1:def_2 .= dom the Charact of A by PARTFUN1:def_2 .= dom the charact of (1-Alg A) by A2, MSUALG_1:def_13 ; hence the charact of (1-Alg B) = Opers ((1-Alg A),S) by A7, UNIALG_2:def_6; ::_thesis: verum end; theorem Th20: :: MSSUBLAT:20 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A let A be non-empty MSAlgebra over MS; ::_thesis: for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A let B be non-empty MSSubAlgebra of A; ::_thesis: 1-Alg B is SubAlgebra of 1-Alg A ( the carrier of (1-Alg B) is Subset of (1-Alg A) & ( for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds ( the charact of (1-Alg B) = Opers ((1-Alg A),S) & S is opers_closed ) ) ) by Th17, Th18, Th19; hence 1-Alg B is SubAlgebra of 1-Alg A by UNIALG_2:def_7; ::_thesis: verum end; theorem Th21: :: MSSUBLAT:21 for S being non empty non void ManySortedSign for A, B being MSAlgebra over S holds ( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B being MSAlgebra over S holds ( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ) let A, B be MSAlgebra over S; ::_thesis: ( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ) thus ( A is MSSubAlgebra of B implies A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ) ::_thesis: ( A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) implies A is MSSubAlgebra of B ) proof assume A1: A is MSSubAlgebra of B ; ::_thesis: A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) hence the Sorts of A is MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) by MSUALG_2:def_9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of B, the Charact of B #) holds ( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),b1) ) ) thus for BB being MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) st BB = the Sorts of A holds ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) ::_thesis: verum proof let BB be MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #); ::_thesis: ( BB = the Sorts of A implies ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) ) assume A2: BB = the Sorts of A ; ::_thesis: ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) reconsider bb = BB as MSSubset of B ; A3: bb is opers_closed by A1, A2, MSUALG_2:def_9; A4: BB is opers_closed proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: BB is_closed_on o A5: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6 .= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ; bb is_closed_on o by A3, MSUALG_2:def_6; then rng ((Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o)) c= (BB * the ResultSort of S) . o by A5, MSUALG_2:def_5; hence BB is_closed_on o by MSUALG_2:def_5; ::_thesis: verum end; for o being set st o in the carrier' of S holds the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o proof let o be set ; ::_thesis: ( o in the carrier' of S implies the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o ) assume o in the carrier' of S ; ::_thesis: the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o then reconsider o = o as OperSymbol of S ; A6: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6 .= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ; A7: bb is_closed_on o by A3, MSUALG_2:def_6; A8: BB is_closed_on o by A4, MSUALG_2:def_6; (Opers (B,bb)) . o = o /. bb by MSUALG_2:def_8 .= (Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o) by A6, A7, MSUALG_2:def_7 .= o /. BB by A8, MSUALG_2:def_7 .= (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o by MSUALG_2:def_8 ; hence the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o by A1, A2, MSUALG_2:def_9; ::_thesis: verum end; hence ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) by A4, PBOOLE:3; ::_thesis: verum end; end; assume A9: A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) ; ::_thesis: A is MSSubAlgebra of B hence the Sorts of A is MSSubset of B by MSUALG_2:def_9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of B holds ( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (B,b1) ) ) let C be MSSubset of B; ::_thesis: ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers (B,C) ) ) assume A10: C = the Sorts of A ; ::_thesis: ( C is opers_closed & the Charact of A = Opers (B,C) ) reconsider CC = C as MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) ; A11: CC is opers_closed by A9, A10, MSUALG_2:def_9; A12: C is opers_closed proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: C is_closed_on o A13: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6 .= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ; CC is_closed_on o by A11, MSUALG_2:def_6; then rng ((Den (o,B)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o by A13, MSUALG_2:def_5; hence C is_closed_on o by MSUALG_2:def_5; ::_thesis: verum end; for o being set st o in the carrier' of S holds the Charact of A . o = (Opers (B,C)) . o proof let o be set ; ::_thesis: ( o in the carrier' of S implies the Charact of A . o = (Opers (B,C)) . o ) assume o in the carrier' of S ; ::_thesis: the Charact of A . o = (Opers (B,C)) . o then reconsider o = o as OperSymbol of S ; A14: Den (o,B) = the Charact of MSAlgebra(# the Sorts of B, the Charact of B #) . o by MSUALG_1:def_6 .= Den (o,MSAlgebra(# the Sorts of B, the Charact of B #)) by MSUALG_1:def_6 ; A15: CC is_closed_on o by A11, MSUALG_2:def_6; A16: C is_closed_on o by A12, MSUALG_2:def_6; (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),CC)) . o = o /. CC by MSUALG_2:def_8 .= (Den (o,B)) | (((C #) * the Arity of S) . o) by A14, A15, MSUALG_2:def_7 .= o /. C by A16, MSUALG_2:def_7 .= (Opers (B,C)) . o by MSUALG_2:def_8 ; hence the Charact of A . o = (Opers (B,C)) . o by A9, A10, MSUALG_2:def_9; ::_thesis: verum end; hence ( C is opers_closed & the Charact of A = Opers (B,C) ) by A12, PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBLAT:22 for A, B being Universal_Algebra holds ( signature A = signature B iff MSSign A = MSSign B ) proof A1: for A, B being Universal_Algebra st MSSign A = MSSign B holds signature A = signature B proof let A, B be Universal_Algebra; ::_thesis: ( MSSign A = MSSign B implies signature A = signature B ) reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2; reconsider gg1 = (*--> 0) * (signature B) as Function of (dom (signature B)),({0} *) by MSUALG_1:2; A2: ( MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) & MSSign B = ManySortedSign(# {0},(dom (signature B)),gg1,((dom (signature B)) --> z) #) ) by MSUALG_1:10; assume A3: MSSign A = MSSign B ; ::_thesis: signature A = signature B now__::_thesis:_for_i_being_Nat_st_i_in_dom_(signature_A)_holds_ (signature_A)_._i_=_(signature_B)_._i let i be Nat; ::_thesis: ( i in dom (signature A) implies (signature A) . i = (signature B) . i ) assume A4: i in dom (signature A) ; ::_thesis: (signature A) . i = (signature B) . i then reconsider k = (signature A) . i as Element of NAT by PARTFUN1:4; A5: i in dom ((*--> 0) * (signature A)) by A4, FINSEQ_3:120; then A6: (*--> 0) . ((signature B) . i) = ((*--> 0) * (signature A)) . i by A3, A2, FINSEQ_3:120 .= (*--> 0) . ((signature A) . i) by A5, FINSEQ_3:120 ; reconsider m = (signature B) . i as Element of NAT by A3, A2, A4, PARTFUN1:4; reconsider q = (*--> 0) . m as FinSequence ; reconsider p = (*--> 0) . k as FinSequence ; thus (signature A) . i = len p by Th6 .= len q by A6 .= (signature B) . i by Th6 ; ::_thesis: verum end; hence signature A = signature B by A3, A2, FINSEQ_1:13; ::_thesis: verum end; for A, B being Universal_Algebra st signature A = signature B holds MSSign A = MSSign B proof let A, B be Universal_Algebra; ::_thesis: ( signature A = signature B implies MSSign A = MSSign B ) assume signature A = signature B ; ::_thesis: MSSign A = MSSign B then A,B are_similar by UNIALG_2:def_1; hence MSSign A = MSSign B by MSUHOM_1:10; ::_thesis: verum end; hence for A, B being Universal_Algebra holds ( signature A = signature B iff MSSign A = MSSign B ) by A1; ::_thesis: verum end; theorem Th23: :: MSSUBLAT:23 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) let A be non-empty MSAlgebra over MS; ::_thesis: ( the carrier of MS = {0} implies MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) ) reconsider ff1 = (*--> 0) * (signature (1-Alg A)) as Function of (dom (signature (1-Alg A))),({0} *) by MSUALG_1:2; A1: MSSign (1-Alg A) = ManySortedSign(# {0},(dom (signature (1-Alg A))),ff1,((dom (signature (1-Alg A))) --> z) #) by MSUALG_1:10; dom the ResultSort of MS = the carrier' of MS by FUNCT_2:def_1; then A2: rng the ResultSort of MS <> {} by RELAT_1:42; consider k being Nat such that A3: the carrier' of MS = Seg k by MSUALG_1:def_7; A4: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14; A5: len (signature (1-Alg A)) = len the charact of (1-Alg A) by UNIALG_1:def_4; then A6: dom (signature (1-Alg A)) = dom the charact of (1-Alg A) by FINSEQ_3:29 .= dom the Charact of A by A4, MSUALG_1:def_13 .= the carrier' of MS by PARTFUN1:def_2 ; then A7: the carrier' of MS = dom ff1 by FUNCT_2:def_1; assume A8: the carrier of MS = {0} ; ::_thesis: MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) A9: for x being set st x in the carrier' of MS holds ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x proof let x be set ; ::_thesis: ( x in the carrier' of MS implies ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x ) assume x in the carrier' of MS ; ::_thesis: ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x then reconsider x = x as OperSymbol of MS ; x in Seg k by A3; then reconsider n = x as Nat ; n in dom (signature (1-Alg A)) by A6; then A10: n in dom the charact of (1-Alg A) by A5, FINSEQ_3:29; then reconsider h = the charact of (1-Alg A) . n as PartFunc of ( the carrier of (1-Alg A) *), the carrier of (1-Alg A) by UNIALG_1:1; reconsider h = h as non empty homogeneous quasi_total PartFunc of ( the carrier of (1-Alg A) *), the carrier of (1-Alg A) by A10, MARGREL1:def_24; set aa = the Element of dom h; set ah = arity h; dom h c= the carrier of (1-Alg A) * by RELAT_1:def_18; then the Element of dom h in the carrier of (1-Alg A) * by TARSKI:def_3; then reconsider bb = the Element of dom h as FinSequence of the carrier of (1-Alg A) by FINSEQ_1:def_11; A11: bb in dom h ; h = the Charact of A . x by A4, MSUALG_1:def_13 .= Den (x,A) by MSUALG_1:def_6 ; then bb in Args (x,A) by A11, FUNCT_2:def_1; then bb in (len (the_arity_of x)) -tuples_on (the_sort_of A) by MSUALG_1:6; then A12: len (the_arity_of x) = len bb by CARD_1:def_7 .= arity h by MARGREL1:def_25 ; ((*--> 0) * (signature (1-Alg A))) . x = (*--> 0) . ((signature (1-Alg A)) . x) by A6, FUNCT_1:13 .= (*--> 0) . (arity h) by A6, UNIALG_1:def_4 .= (arity h) |-> 0 by FINSEQ_2:def_6 .= the_arity_of x by A8, A12, Th5 .= the Arity of MS . x by MSUALG_1:def_1 ; hence ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x ; ::_thesis: verum end; rng the ResultSort of MS c= {0} by A8, RELAT_1:def_19; then ( the carrier' of MS = dom the ResultSort of MS & rng the ResultSort of MS = {0} ) by A2, FUNCT_2:def_1, ZFMISC_1:33; then ( the carrier' of MS = dom the Arity of MS & the ResultSort of (MSSign (1-Alg A)) = the ResultSort of MS ) by A1, A6, FUNCOP_1:9, FUNCT_2:def_1; hence MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) by A8, A1, A6, A7, A9, FUNCT_1:2; ::_thesis: verum end; theorem Th24: :: MSSUBLAT:24 for MS being non void 1 -element segmental ManySortedSign for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) let A, B be non-empty MSAlgebra over MS; ::_thesis: ( 1-Alg A = 1-Alg B implies MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ) assume A1: 1-Alg A = 1-Alg B ; ::_thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) A2: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def_14; A3: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14; A4: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_MS_holds_ the_Sorts_of_A_._i_=_the_Sorts_of_B_._i let i be set ; ::_thesis: ( i in the carrier of MS implies the Sorts of A . i = the Sorts of B . i ) assume A5: i in the carrier of MS ; ::_thesis: the Sorts of A . i = the Sorts of B . i A6: ex c being Component of the Sorts of B st the Sorts of B . i = c proof reconsider c = the Sorts of B . i as Component of the Sorts of B by A5, PBOOLE:139; take c ; ::_thesis: the Sorts of B . i = c thus the Sorts of B . i = c ; ::_thesis: verum end; ex c being Component of the Sorts of A st the Sorts of A . i = c proof reconsider c = the Sorts of A . i as Component of the Sorts of A by A5, PBOOLE:139; take c ; ::_thesis: the Sorts of A . i = c thus the Sorts of A . i = c ; ::_thesis: verum end; then the Sorts of A . i = the_sort_of B by A1, A3, A2, MSUALG_1:def_12 .= the Sorts of B . i by A6, MSUALG_1:def_12 ; hence the Sorts of A . i = the Sorts of B . i ; ::_thesis: verum end; the Charact of A = the charact of (1-Alg A) by A3, MSUALG_1:def_13 .= the Charact of B by A1, A2, MSUALG_1:def_13 ; hence MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) by A4, PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBLAT:25 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds the Sorts of A = the Sorts of (MSAlg (1-Alg A)) proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds the Sorts of A = the Sorts of (MSAlg (1-Alg A)) let A be non-empty MSAlgebra over MS; ::_thesis: ( the carrier of MS = {0} implies the Sorts of A = the Sorts of (MSAlg (1-Alg A)) ) assume A1: the carrier of MS = {0} ; ::_thesis: the Sorts of A = the Sorts of (MSAlg (1-Alg A)) A2: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_MS_holds_ the_Sorts_of_A_._i_=_({0}_-->_(the_sort_of_A))_._i let i be set ; ::_thesis: ( i in the carrier of MS implies the Sorts of A . i = ({0} --> (the_sort_of A)) . i ) assume A3: i in the carrier of MS ; ::_thesis: the Sorts of A . i = ({0} --> (the_sort_of A)) . i A4: ex c being Component of the Sorts of A st the Sorts of A . i = c proof reconsider c = the Sorts of A . i as Component of the Sorts of A by A3, PBOOLE:139; take c ; ::_thesis: the Sorts of A . i = c thus the Sorts of A . i = c ; ::_thesis: verum end; ({0} --> (the_sort_of A)) . i = the_sort_of A by A1, A3, FUNCOP_1:7; hence the Sorts of A . i = ({0} --> (the_sort_of A)) . i by A4, MSUALG_1:def_12; ::_thesis: verum end; 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def_14; then A5: ( MSAlg (1-Alg A) = MSAlgebra(# (MSSorts (1-Alg A)),(MSCharact (1-Alg A)) #) & MSSorts (1-Alg A) = 0 .--> (the_sort_of A) ) by MSUALG_1:def_9, MSUALG_1:def_11; {0} --> (the_sort_of A) is ManySortedSet of the carrier of MS by A1; hence the Sorts of A = the Sorts of (MSAlg (1-Alg A)) by A5, A2, PBOOLE:3; ::_thesis: verum end; theorem Th26: :: MSSUBLAT:26 for MS being non void 1 -element segmental ManySortedSign for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) proof let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) let A be non-empty MSAlgebra over MS; ::_thesis: ( the carrier of MS = {0} implies MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) ) reconsider c = the_sort_of (MSAlg (1-Alg A)) as Component of the Sorts of (MSAlg (1-Alg A)) by MSUALG_1:def_12; assume the carrier of MS = {0} ; ::_thesis: MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) then MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) by Th23; then reconsider M1A = MSAlg (1-Alg A) as strict MSAlgebra over MS ; reconsider M1A = M1A as strict non-empty MSAlgebra over MS by MSUALG_1:def_3; A1: 1-Alg M1A = UAStr(# (the_sort_of M1A),(the_charact_of M1A) #) by MSUALG_1:def_14; reconsider c = c as Component of the Sorts of M1A ; A2: 1-Alg (MSAlg (1-Alg A)) = UAStr(# (the_sort_of (MSAlg (1-Alg A))),(the_charact_of (MSAlg (1-Alg A))) #) by MSUALG_1:def_14; then A3: the charact of (1-Alg A) = the_charact_of (MSAlg (1-Alg A)) by MSUALG_1:9 .= the Charact of M1A by MSUALG_1:def_13 .= the charact of (1-Alg M1A) by A1, MSUALG_1:def_13 ; c = the_sort_of M1A by MSUALG_1:def_12; then the carrier of (1-Alg A) = the carrier of (1-Alg M1A) by A2, A1, MSUALG_1:9; hence MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) by A3, Th24; ::_thesis: verum end; theorem :: MSSUBLAT:27 for A being Universal_Algebra for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds 1-Alg B is SubAlgebra of A proof let A be Universal_Algebra; ::_thesis: for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds 1-Alg B is SubAlgebra of A let B be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( the carrier of (MSSign A) = {0} implies 1-Alg B is SubAlgebra of A ) assume the carrier of (MSSign A) = {0} ; ::_thesis: 1-Alg B is SubAlgebra of A then MSAlg (1-Alg B) = MSAlgebra(# the Sorts of B, the Charact of B #) by Th26; hence 1-Alg B is SubAlgebra of A by Th16; ::_thesis: verum end; begin theorem Th28: :: MSSUBLAT:28 for A being Universal_Algebra for a1, b1 being strict SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) proof let A be Universal_Algebra; ::_thesis: for a1, b1 being strict SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) let a1, b1 be strict SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) ) assume that A1: a2 = MSAlg a1 and A2: b2 = MSAlg b1 ; ::_thesis: the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def_11; then A3: the Sorts of a2 = 0 .--> the carrier of a1 by MSUALG_1:def_9; reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2; A4: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10; then reconsider W = 0 .--> ( the carrier of a1 \/ the carrier of b1) as ManySortedSet of the carrier of (MSSign A) ; A5: b2 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #) by A2, MSUALG_1:def_11; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(MSSign_A)_holds_ W_._x_=_(_the_Sorts_of_a2_._x)_\/_(_the_Sorts_of_b2_._x) let x be set ; ::_thesis: ( x in the carrier of (MSSign A) implies W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) ) assume A6: x in the carrier of (MSSign A) ; ::_thesis: W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) then A7: x = 0 by A4, TARSKI:def_1; W . x = (0 .--> ( the carrier of a1 \/ the carrier of b1)) . 0 by A4, A6, TARSKI:def_1 .= the carrier of a1 \/ the carrier of b1 by FUNCOP_1:72 .= ((0 .--> the carrier of a1) . 0) \/ the carrier of b1 by FUNCOP_1:72 .= ((0 .--> the carrier of a1) . 0) \/ ((0 .--> the carrier of b1) . 0) by FUNCOP_1:72 .= ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) by A3, A5, A7, MSUALG_1:def_9 ; hence W . x = ( the Sorts of a2 . x) \/ ( the Sorts of b2 . x) ; ::_thesis: verum end; hence the Sorts of a2 \/ the Sorts of b2 = 0 .--> ( the carrier of a1 \/ the carrier of b1) by PBOOLE:def_4; ::_thesis: verum end; theorem Th29: :: MSSUBLAT:29 for A being Universal_Algebra for a1, b1 being strict non-empty SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) proof let A be Universal_Algebra; ::_thesis: for a1, b1 being strict non-empty SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) let a1, b1 be strict non-empty SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) ) assume that A1: a2 = MSAlg a1 and A2: b2 = MSAlg b1 ; ::_thesis: the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def_11; then A3: the Sorts of a2 = 0 .--> the carrier of a1 by MSUALG_1:def_9; reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2; A4: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10; then reconsider W = 0 .--> ( the carrier of a1 /\ the carrier of b1) as ManySortedSet of the carrier of (MSSign A) ; A5: b2 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #) by A2, MSUALG_1:def_11; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(MSSign_A)_holds_ W_._x_=_(_the_Sorts_of_a2_._x)_/\_(_the_Sorts_of_b2_._x) let x be set ; ::_thesis: ( x in the carrier of (MSSign A) implies W . x = ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) ) assume x in the carrier of (MSSign A) ; ::_thesis: W . x = ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) then A6: x = 0 by A4, TARSKI:def_1; then W . x = the carrier of a1 /\ the carrier of b1 by FUNCOP_1:72 .= ((0 .--> the carrier of a1) . 0) /\ the carrier of b1 by FUNCOP_1:72 .= ((0 .--> the carrier of a1) . 0) /\ ((0 .--> the carrier of b1) . 0) by FUNCOP_1:72 .= ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) by A3, A5, A6, MSUALG_1:def_9 ; hence W . x = ( the Sorts of a2 . x) /\ ( the Sorts of b2 . x) ; ::_thesis: verum end; hence the Sorts of a2 /\ the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1) by PBOOLE:def_5; ::_thesis: verum end; theorem Th30: :: MSSUBLAT:30 for A being strict Universal_Algebra for a1, b1 being strict non-empty SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 "\/" b1) = a2 "\/" b2 proof let A be strict Universal_Algebra; ::_thesis: for a1, b1 being strict non-empty SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 "\/" b1) = a2 "\/" b2 let a1, b1 be strict non-empty SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 "\/" b1) = a2 "\/" b2 reconsider MSA = MSAlg (a1 "\/" b1) as MSSubAlgebra of MSAlg A by Th12; let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 "\/" b1) = a2 "\/" b2 ) assume that A1: a2 = MSAlg a1 and A2: b2 = MSAlg b1 ; ::_thesis: MSAlg (a1 "\/" b1) = a2 "\/" b2 MSSign (a1 "\/" b1) = MSSign A by Th7; then reconsider MSA = MSA as strict non-empty MSSubAlgebra of MSAlg A ; for B being MSSubset of (MSAlg A) st B = the Sorts of a2 \/ the Sorts of b2 holds MSA = GenMSAlg B proof ( the carrier of a1 is Subset of A & the carrier of b1 is Subset of A ) by UNIALG_2:def_7; then reconsider K = the carrier of a1 \/ the carrier of b1 as non empty Subset of A by XBOOLE_1:8; reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2; set X = MSA; reconsider M1 = the Sorts of MSA as ManySortedSet of the carrier of (MSSign A) ; A3: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10; then reconsider x = 0 as Element of (MSSign A) ; let B be MSSubset of (MSAlg A); ::_thesis: ( B = the Sorts of a2 \/ the Sorts of b2 implies MSA = GenMSAlg B ) assume A4: B = the Sorts of a2 \/ the Sorts of b2 ; ::_thesis: MSA = GenMSAlg B A5: for U1 being MSSubAlgebra of MSAlg A st B is MSSubset of U1 holds MSA is MSSubAlgebra of U1 proof let U1 be MSSubAlgebra of MSAlg A; ::_thesis: ( B is MSSubset of U1 implies MSA is MSSubAlgebra of U1 ) assume A6: B is MSSubset of U1 ; ::_thesis: MSA is MSSubAlgebra of U1 percases ( U1 is non-empty or not U1 is non-empty ) ; suppose U1 is non-empty ; ::_thesis: MSA is MSSubAlgebra of U1 then reconsider U11 = U1 as non-empty MSSubAlgebra of MSAlg A ; A7: 1-Alg U11 is SubAlgebra of 1-Alg (MSAlg A) by Th20; then reconsider A1 = 1-Alg U11 as strict SubAlgebra of A by MSUALG_1:9; B c= the Sorts of U11 by A6, PBOOLE:def_18; then A8: B . x c= the Sorts of U11 . x by PBOOLE:def_2; ( MSAlgebra(# the Sorts of U11, the Charact of U11 #) = MSAlg (1-Alg U11) & MSAlg (1-Alg U11) = MSAlgebra(# (MSSorts (1-Alg U11)),(MSCharact (1-Alg U11)) #) ) by A3, Th26, MSUALG_1:def_11; then A9: the Sorts of U11 . 0 = (0 .--> the carrier of (1-Alg U11)) . 0 by MSUALG_1:def_9; B . 0 = (0 .--> K) . 0 by A1, A2, A4, Th28 .= K by FUNCOP_1:72 ; then the carrier of a1 \/ the carrier of b1 c= the carrier of A1 by A8, A9, FUNCOP_1:72; then GenUnivAlg K is SubAlgebra of 1-Alg U11 by UNIALG_2:def_12; then a1 "\/" b1 is SubAlgebra of 1-Alg U11 by UNIALG_2:def_13; then A10: MSA is MSSubAlgebra of MSAlg (1-Alg U11) by Th12; 1-Alg U11 is SubAlgebra of A by A7, MSUALG_1:9; then MSSign A = MSSign (1-Alg U11) by Th7; then MSA is MSSubAlgebra of MSAlgebra(# the Sorts of U11, the Charact of U11 #) by A3, A10, Th26; hence MSA is MSSubAlgebra of U1 by Th21; ::_thesis: verum end; suppose not U1 is non-empty ; ::_thesis: MSA is MSSubAlgebra of U1 then the Sorts of U1 is V2() by MSUALG_1:def_3; then A11: ex i being set st ( i in the carrier of (MSSign A) & the Sorts of U1 . i is empty ) by PBOOLE:def_13; reconsider 0a1 = 0 .--> the carrier of a1 as ManySortedSet of the carrier of (MSSign A) by A3; set e = the Element of a1; B c= the Sorts of U1 by A6, PBOOLE:def_18; then A12: B . x c= the Sorts of U1 . x by PBOOLE:def_2; a2 = MSAlgebra(# (MSSorts a1),(MSCharact a1) #) by A1, MSUALG_1:def_11; then B = 0a1 \/ the Sorts of b2 by A4, MSUALG_1:def_9; then A13: B . x = (0a1 . x) \/ ( the Sorts of b2 . x) by PBOOLE:def_4; x in {0} by TARSKI:def_1; then 0a1 . x = the carrier of a1 by FUNCOP_1:7; then the Element of a1 in B . x by A13, XBOOLE_0:def_3; hence MSA is MSSubAlgebra of U1 by A3, A11, A12, TARSKI:def_1; ::_thesis: verum end; end; end; MSA = MSAlgebra(# (MSSorts (a1 "\/" b1)),(MSCharact (a1 "\/" b1)) #) by MSUALG_1:def_11; then A14: the Sorts of MSA = 0 .--> the carrier of (a1 "\/" b1) by MSUALG_1:def_9; the Sorts of a2 \/ the Sorts of b2 c= M1 proof let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of (MSSign A) or ( the Sorts of a2 \/ the Sorts of b2) . x c= M1 . x ) A15: a1 "\/" b1 = GenUnivAlg K by UNIALG_2:def_13; assume A16: x in the carrier of (MSSign A) ; ::_thesis: ( the Sorts of a2 \/ the Sorts of b2) . x c= M1 . x then A17: M1 . x = (0 .--> the carrier of (a1 "\/" b1)) . 0 by A14, A3, TARSKI:def_1 .= the carrier of (a1 "\/" b1) by FUNCOP_1:72 ; ( the Sorts of a2 \/ the Sorts of b2) . x = ( the Sorts of a2 \/ the Sorts of b2) . 0 by A3, A16, TARSKI:def_1 .= (0 .--> ( the carrier of a1 \/ the carrier of b1)) . 0 by A1, A2, Th28 .= the carrier of a1 \/ the carrier of b1 by FUNCOP_1:72 ; hence ( the Sorts of a2 \/ the Sorts of b2) . x c= M1 . x by A17, A15, UNIALG_2:def_12; ::_thesis: verum end; then B is MSSubset of MSA by A4, PBOOLE:def_18; hence MSA = GenMSAlg B by A5, MSUALG_2:def_17; ::_thesis: verum end; hence MSAlg (a1 "\/" b1) = a2 "\/" b2 by MSUALG_2:def_18; ::_thesis: verum end; registration let A be with_const_op Universal_Algebra; cluster MSSign A -> all-with_const_op ; coherence ( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op ) proof reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2; A1: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10; MSSign A is all-with_const_op proof let s be SortSymbol of (MSSign A); :: according to MSUALG_2:def_2 ::_thesis: s is with_const_op consider OO being operation of A such that A2: arity OO = 0 by UNIALG_2:def_11; Seg (len the charact of A) = dom the charact of A by FINSEQ_1:def_3; then consider i being Nat such that A3: i in Seg (len the charact of A) and A4: the charact of A . i = OO by FINSEQ_2:10; A5: len (signature A) = len the charact of A by UNIALG_1:def_4; then A6: i in dom (signature A) by A3, FINSEQ_1:def_3; reconsider i = i as OperSymbol of (MSSign A) by A1, A3, A5, FINSEQ_1:def_3; take i ; :: according to MSUALG_2:def_1 ::_thesis: ( the Arity of (MSSign A) . i = {} & the ResultSort of (MSSign A) . i = s ) (*--> 0) . ((signature A) . i) = (*--> 0) . 0 by A2, A4, A6, UNIALG_1:def_4 .= {} by Th1 ; hence the Arity of (MSSign A) . i = {} by A1, FUNCT_1:13; ::_thesis: the ResultSort of (MSSign A) . i = s the ResultSort of (MSSign A) . i = 0 by A1, TARSKI:def_1; hence the ResultSort of (MSSign A) . i = s by A1, TARSKI:def_1; ::_thesis: verum end; hence ( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op ) ; ::_thesis: verum end; end; theorem Th31: :: MSSUBLAT:31 for A being with_const_op Universal_Algebra for a1, b1 being strict non-empty SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 /\ b1) = a2 /\ b2 proof let A be with_const_op Universal_Algebra; ::_thesis: for a1, b1 being strict non-empty SubAlgebra of A for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 /\ b1) = a2 /\ b2 let a1, b1 be strict non-empty SubAlgebra of A; ::_thesis: for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 /\ b1) = a2 /\ b2 reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2; A1: MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:10; MSAlg (a1 /\ b1) = MSAlgebra(# (MSSorts (a1 /\ b1)),(MSCharact (a1 /\ b1)) #) by MSUALG_1:def_11; then A2: the Sorts of (MSAlg (a1 /\ b1)) = 0 .--> the carrier of (a1 /\ b1) by MSUALG_1:def_9; then dom the Sorts of (MSAlg (a1 /\ b1)) = the carrier of (MSSign A) by A1, FUNCOP_1:13; then reconsider D = the Sorts of (MSAlg (a1 /\ b1)) as ManySortedSet of the carrier of (MSSign A) by PARTFUN1:def_2, RELAT_1:def_18; let a2, b2 be strict non-empty MSSubAlgebra of MSAlg A; ::_thesis: ( a2 = MSAlg a1 & b2 = MSAlg b1 implies MSAlg (a1 /\ b1) = a2 /\ b2 ) assume A3: ( a2 = MSAlg a1 & b2 = MSAlg b1 ) ; ::_thesis: MSAlg (a1 /\ b1) = a2 /\ b2 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(MSSign_A)_holds_ D_._x_=_(_the_Sorts_of_a2_/\_the_Sorts_of_b2)_._x let x be set ; ::_thesis: ( x in the carrier of (MSSign A) implies D . x = ( the Sorts of a2 /\ the Sorts of b2) . x ) A4: the carrier of a1 meets the carrier of b1 by UNIALG_2:17; assume A5: x in the carrier of (MSSign A) ; ::_thesis: D . x = ( the Sorts of a2 /\ the Sorts of b2) . x hence D . x = (0 .--> the carrier of (a1 /\ b1)) . 0 by A2, A1, TARSKI:def_1 .= the carrier of (a1 /\ b1) by FUNCOP_1:72 .= the carrier of a1 /\ the carrier of b1 by A4, UNIALG_2:def_9 .= (0 .--> ( the carrier of a1 /\ the carrier of b1)) . 0 by FUNCOP_1:72 .= ( the Sorts of a2 /\ the Sorts of b2) . 0 by A3, Th29 .= ( the Sorts of a2 /\ the Sorts of b2) . x by A1, A5, TARSKI:def_1 ; ::_thesis: verum end; then A6: D = the Sorts of a2 /\ the Sorts of b2 by PBOOLE:3; MSSign (a1 /\ b1) = MSSign A by Th7; then reconsider AA = MSAlg (a1 /\ b1) as strict non-empty MSSubAlgebra of MSAlg A by Th12; for B being MSSubset of (MSAlg A) st B = the Sorts of AA holds ( B is opers_closed & the Charact of AA = Opers ((MSAlg A),B) ) by MSUALG_2:def_9; hence MSAlg (a1 /\ b1) = a2 /\ b2 by A6, MSUALG_2:def_16; ::_thesis: verum end; registration let A be quasi_total UAStr ; cluster UAStr(# the carrier of A, the charact of A #) -> quasi_total ; coherence UAStr(# the carrier of A, the charact of A #) is quasi_total proof thus the charact of UAStr(# the carrier of A, the charact of A #) is quasi_total ; :: according to UNIALG_1:def_2 ::_thesis: verum end; end; registration let A be partial UAStr ; cluster UAStr(# the carrier of A, the charact of A #) -> partial ; coherence UAStr(# the carrier of A, the charact of A #) is partial proof thus the charact of UAStr(# the carrier of A, the charact of A #) is homogeneous ; :: according to UNIALG_1:def_1 ::_thesis: verum end; end; registration let A be non-empty UAStr ; cluster UAStr(# the carrier of A, the charact of A #) -> non-empty ; coherence UAStr(# the carrier of A, the charact of A #) is non-empty proof thus ( the charact of UAStr(# the carrier of A, the charact of A #) <> {} & the charact of UAStr(# the carrier of A, the charact of A #) is non-empty ) ; :: according to UNIALG_1:def_3 ::_thesis: verum end; end; registration let A be with_const_op Universal_Algebra; cluster UAStr(# the carrier of A, the charact of A #) -> with_const_op ; coherence UAStr(# the carrier of A, the charact of A #) is with_const_op proof consider o being operation of A such that A1: arity o = 0 by UNIALG_2:def_11; reconsider oo = o as operation of UAStr(# the carrier of A, the charact of A #) ; take oo ; :: according to UNIALG_2:def_11 ::_thesis: arity oo = 0 thus arity oo = 0 by A1; ::_thesis: verum end; end; theorem :: MSSUBLAT:32 for A being with_const_op Universal_Algebra holds UnSubAlLattice UAStr(# the carrier of A, the charact of A #), MSSubAlLattice (MSAlg UAStr(# the carrier of A, the charact of A #)) are_isomorphic proof let Z be with_const_op Universal_Algebra; ::_thesis: UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) are_isomorphic set A = UAStr(# the carrier of Z, the charact of Z #); reconsider ff1 = (*--> 0) * (signature UAStr(# the carrier of Z, the charact of Z #)) as Function of (dom (signature UAStr(# the carrier of Z, the charact of Z #))),({0} *) by MSUALG_1:2; A1: MSSign UAStr(# the carrier of Z, the charact of Z #) = ManySortedSign(# {0},(dom (signature UAStr(# the carrier of Z, the charact of Z #))),ff1,((dom (signature UAStr(# the carrier of Z, the charact of Z #))) --> z) #) by MSUALG_1:10; defpred S1[ set , set ] means ex A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st ( A1 = \$1 & \$2 = MSAlg A1 ); A2: for x being Element of Sub UAStr(# the carrier of Z, the charact of Z #) ex y being Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) st S1[x,y] proof let x be Element of Sub UAStr(# the carrier of Z, the charact of Z #); ::_thesis: ex y being Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) st S1[x,y] reconsider B = x as strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14; MSSign UAStr(# the carrier of Z, the charact of Z #) = MSSign B by Th7; then MSAlg B is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12; then reconsider y = MSAlg B as Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) by MSUALG_2:def_19; take y ; ::_thesis: S1[x,y] take B ; ::_thesis: ( B = x & y = MSAlg B ) thus ( B = x & y = MSAlg B ) ; ::_thesis: verum end; consider f being Function of (Sub UAStr(# the carrier of Z, the charact of Z #)),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))) such that A3: for x being Element of Sub UAStr(# the carrier of Z, the charact of Z #) holds S1[x,f . x] from FUNCT_2:sch_3(A2); reconsider f = f as Function of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) ; f is Homomorphism of UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) proof let a1, b1 be Element of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)); :: according to LATTICE4:def_1 ::_thesis: ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) reconsider a2 = a1, b2 = b1 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) ; reconsider a3 = a2, b3 = b2 as strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14; reconsider s = a3 "\/" b3 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14; reconsider m = a3 /\ b3 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14; A4: ex A1 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st ( A1 = s & f . s = MSAlg A1 ) by A3; MSSign b3 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7; then reconsider g2 = MSAlg b3 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12; consider A4 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that A5: A4 = b3 and A6: f . b3 = MSAlg A4 by A3; MSSign A4 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7; then reconsider g3 = MSAlg A4 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12; MSSign a3 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7; then reconsider g1 = MSAlg a3 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12; consider A3 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that A7: A3 = a3 and A8: f . a3 = MSAlg A3 by A3; MSSign A3 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7; then reconsider g4 = MSAlg A3 as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by Th12; A9: ex A1 being strict non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st ( A1 = m & f . m = MSAlg A1 ) by A3; A10: f . (a1 "/\" b1) = f . ((UniAlg_meet UAStr(# the carrier of Z, the charact of Z #)) . (a2,b2)) by LATTICES:def_2 .= MSAlg (a3 /\ b3) by A9, UNIALG_2:def_16 .= g1 /\ g2 by Th31 .= the L_meet of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . ((f . a1),(f . b1)) by A7, A8, A5, A6, MSUALG_2:def_21 .= (f . a1) "/\" (f . b1) by LATTICES:def_2 ; f . (a1 "\/" b1) = f . ((UniAlg_join UAStr(# the carrier of Z, the charact of Z #)) . (a2,b2)) by LATTICES:def_1 .= MSAlg (a3 "\/" b3) by A4, UNIALG_2:def_15 .= g4 "\/" g3 by A7, A5, Th30 .= the L_join of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . ((f . a1),(f . b1)) by A8, A6, MSUALG_2:def_20 .= (f . a1) "\/" (f . b1) by LATTICES:def_1 ; hence ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) by A10; ::_thesis: verum end; then reconsider f = f as Homomorphism of UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) ; take f ; :: according to LATTICE4:def_2 ::_thesis: f is bijective now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A11: ( x1 in dom f & x2 in dom f ) and A12: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider y1 = x1, y2 = x2 as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by A11, FUNCT_2:def_1; consider A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that A13: A1 = y1 and A14: f . y1 = MSAlg A1 by A3; consider A2 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) such that A15: ( A2 = y2 & f . y2 = MSAlg A2 ) by A3; A16: MSSign A1 = MSSign UAStr(# the carrier of Z, the charact of Z #) by Th7 .= MSSign A2 by Th7 ; thus x1 = 1-Alg (MSAlg A1) by A13, MSUALG_1:9 .= x2 by A12, A14, A15, A16, MSUALG_1:9 ; ::_thesis: verum end; hence f is one-to-one by FUNCT_1:def_4; :: according to FUNCT_2:def_4 ::_thesis: f is onto A17: dom f = Sub UAStr(# the carrier of Z, the charact of Z #) by FUNCT_2:def_1; thus rng f = the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) :: according to FUNCT_2:def_3 ::_thesis: verum proof thus rng f c= the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) c= rng f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) or x in rng f ) assume x in the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) ; ::_thesis: x in rng f then reconsider y = x as strict MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by MSUALG_2:def_19; reconsider C = Constants (MSAlg UAStr(# the carrier of Z, the charact of Z #)) as MSSubset of y by MSUALG_2:10; C c= the Sorts of y by PBOOLE:def_18; then the Sorts of y is V2() by PBOOLE:131; then reconsider y = y as strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #) by MSUALG_1:def_3; 1-Alg y is SubAlgebra of 1-Alg (MSAlg UAStr(# the carrier of Z, the charact of Z #)) by Th20; then 1-Alg y is SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) by MSUALG_1:9; then reconsider y1 = 1-Alg y as Element of Sub UAStr(# the carrier of Z, the charact of Z #) by UNIALG_2:def_14; ex A1 being strict SubAlgebra of UAStr(# the carrier of Z, the charact of Z #) st ( A1 = y1 & f . y1 = MSAlg A1 ) by A3; then A18: f . (1-Alg y) = x by A1, Th26; y1 in dom f by A17; hence x in rng f by A18, FUNCT_1:def_3; ::_thesis: verum end; end;