:: UNIALG_2 semantic presentation begin definition let U1 be Universal_Algebra; mode PFuncsDomHQN of U1 is PFuncsDomHQN of the carrier of U1; end; definition let U1 be UAStr ; mode PartFunc of U1 is PartFunc of ( the carrier of U1 *), the carrier of U1; end; definition let U1, U2 be Universal_Algebra; predU1,U2 are_similar means :Def1: :: UNIALG_2:def 1 signature U1 = signature U2; symmetry for U1, U2 being Universal_Algebra st signature U1 = signature U2 holds signature U2 = signature U1 ; reflexivity for U1 being Universal_Algebra holds signature U1 = signature U1 ; end; :: deftheorem Def1 defines are_similar UNIALG_2:def_1_:_ for U1, U2 being Universal_Algebra holds ( U1,U2 are_similar iff signature U1 = signature U2 ); theorem :: UNIALG_2:1 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds len the charact of U1 = len the charact of U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies len the charact of U1 = len the charact of U2 ) A1: ( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def_4; assume U1,U2 are_similar ; ::_thesis: len the charact of U1 = len the charact of U2 hence len the charact of U1 = len the charact of U2 by A1, Def1; ::_thesis: verum end; theorem :: UNIALG_2:2 for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds U1,U3 are_similar proof let U1, U2, U3 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar ) assume ( U1,U2 are_similar & U2,U3 are_similar ) ; ::_thesis: U1,U3 are_similar then ( signature U1 = signature U2 & signature U2 = signature U3 ) by Def1; hence U1,U3 are_similar by Def1; ::_thesis: verum end; theorem :: UNIALG_2:3 for U0 being Universal_Algebra holds rng the charact of U0 is non empty Subset of (PFuncs (( the carrier of U0 *), the carrier of U0)) by FINSEQ_1:def_4, RELAT_1:41; definition let U0 be Universal_Algebra; func Operations U0 -> PFuncsDomHQN of U0 equals :: UNIALG_2:def 2 rng the charact of U0; coherence rng the charact of U0 is PFuncsDomHQN of U0 proof reconsider A = rng the charact of U0 as non empty set by RELAT_1:41; now__::_thesis:_for_x_being_Element_of_A_holds_x_is_non_empty_homogeneous_quasi_total_PartFunc_of_U0 let x be Element of A; ::_thesis: x is non empty homogeneous quasi_total PartFunc of U0 consider i being Nat such that A1: i in dom the charact of U0 and A2: the charact of U0 . i = x by FINSEQ_2:10; reconsider p = the charact of U0 . i as PartFunc of U0 by A1, UNIALG_1:1; ( p is homogeneous & p is quasi_total & not p is empty ) by A1, FUNCT_1:def_9, MARGREL1:def_24; hence x is non empty homogeneous quasi_total PartFunc of U0 by A2; ::_thesis: verum end; hence rng the charact of U0 is PFuncsDomHQN of U0 by MARGREL1:def_26; ::_thesis: verum end; end; :: deftheorem defines Operations UNIALG_2:def_2_:_ for U0 being Universal_Algebra holds Operations U0 = rng the charact of U0; definition let U1 be Universal_Algebra; mode operation of U1 is Element of Operations U1; end; definition let U0 be Universal_Algebra; let A be Subset of U0; let o be operation of U0; predA is_closed_on o means :Def3: :: UNIALG_2:def 3 for s being FinSequence of A st len s = arity o holds o . s in A; end; :: deftheorem Def3 defines is_closed_on UNIALG_2:def_3_:_ for U0 being Universal_Algebra for A being Subset of U0 for o being operation of U0 holds ( A is_closed_on o iff for s being FinSequence of A st len s = arity o holds o . s in A ); definition let U0 be Universal_Algebra; let A be Subset of U0; attrA is opers_closed means :Def4: :: UNIALG_2:def 4 for o being operation of U0 holds A is_closed_on o; end; :: deftheorem Def4 defines opers_closed UNIALG_2:def_4_:_ for U0 being Universal_Algebra for A being Subset of U0 holds ( A is opers_closed iff for o being operation of U0 holds A is_closed_on o ); definition let U0 be Universal_Algebra; let A be non empty Subset of U0; let o be operation of U0; assume A1: A is_closed_on o ; funco /. A -> non empty homogeneous quasi_total PartFunc of (A *),A equals :Def5: :: UNIALG_2:def 5 o | ((arity o) -tuples_on A); coherence o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A proof A2: (arity o) -tuples_on A c= (arity o) -tuples_on the carrier of U0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (arity o) -tuples_on A or x in (arity o) -tuples_on the carrier of U0 ) assume x in (arity o) -tuples_on A ; ::_thesis: x in (arity o) -tuples_on the carrier of U0 then x in { s where s is Element of A * : len s = arity o } by FINSEQ_2:def_4; then consider s being Element of A * such that A3: x = s and A4: len s = arity o ; rng s c= A by FINSEQ_1:def_4; then rng s c= the carrier of U0 by XBOOLE_1:1; then reconsider s = s as FinSequence of the carrier of U0 by FINSEQ_1:def_4; reconsider s = s as Element of the carrier of U0 * by FINSEQ_1:def_11; x = s by A3; then x in { s1 where s1 is Element of the carrier of U0 * : len s1 = arity o } by A4; hence x in (arity o) -tuples_on the carrier of U0 by FINSEQ_2:def_4; ::_thesis: verum end; A5: dom (o | ((arity o) -tuples_on A)) = (dom o) /\ ((arity o) -tuples_on A) by RELAT_1:61 .= ((arity o) -tuples_on the carrier of U0) /\ ((arity o) -tuples_on A) by MARGREL1:22 .= (arity o) -tuples_on A by A2, XBOOLE_1:28 ; A6: rng (o | ((arity o) -tuples_on A)) c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (o | ((arity o) -tuples_on A)) or x in A ) assume x in rng (o | ((arity o) -tuples_on A)) ; ::_thesis: x in A then consider y being set such that A7: y in dom (o | ((arity o) -tuples_on A)) and A8: x = (o | ((arity o) -tuples_on A)) . y by FUNCT_1:def_3; y in { s where s is Element of A * : len s = arity o } by A5, A7, FINSEQ_2:def_4; then consider s being Element of A * such that A9: y = s and A10: len s = arity o ; (o | ((arity o) -tuples_on A)) . s = o . s by A7, A9, FUNCT_1:47; hence x in A by A1, A8, A9, A10, Def3; ::_thesis: verum end; (arity o) -tuples_on A in { (i -tuples_on A) where i is Element of NAT : verum } ; then (arity o) -tuples_on A c= union { (i -tuples_on A) where i is Element of NAT : verum } by ZFMISC_1:74; then dom (o | ((arity o) -tuples_on A)) c= A * by A5, FINSEQ_2:108; then reconsider oa = o | ((arity o) -tuples_on A) as PartFunc of (A *),A by A6, RELSET_1:4; A11: oa is homogeneous proof let x1, y1 be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x1 in dom oa or not y1 in dom oa or len x1 = len y1 ) assume that A12: x1 in dom oa and A13: y1 in dom oa ; ::_thesis: len x1 = len y1 y1 in { s1 where s1 is Element of A * : len s1 = arity o } by A5, A13, FINSEQ_2:def_4; then A14: ex s1 being Element of A * st ( y1 = s1 & len s1 = arity o ) ; x1 in { s where s is Element of A * : len s = arity o } by A5, A12, FINSEQ_2:def_4; then ex s being Element of A * st ( x1 = s & len s = arity o ) ; hence len x1 = len y1 by A14; ::_thesis: verum end; oa is quasi_total proof let x1 be FinSequence of A; :: according to MARGREL1:def_22 ::_thesis: for b1 being FinSequence of A holds ( not len x1 = len b1 or not x1 in dom oa or b1 in dom oa ) let y1 be FinSequence of A; ::_thesis: ( not len x1 = len y1 or not x1 in dom oa or y1 in dom oa ) assume that A15: len x1 = len y1 and A16: x1 in dom oa ; ::_thesis: y1 in dom oa x1 in { s where s is Element of A * : len s = arity o } by A5, A16, FINSEQ_2:def_4; then ex s being Element of A * st ( x1 = s & len s = arity o ) ; then y1 is Element of (arity o) -tuples_on A by A15, FINSEQ_2:92; hence y1 in dom oa by A5; ::_thesis: verum end; hence o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A by A5, A11; ::_thesis: verum end; end; :: deftheorem Def5 defines /. UNIALG_2:def_5_:_ for U0 being Universal_Algebra for A being non empty Subset of U0 for o being operation of U0 st A is_closed_on o holds o /. A = o | ((arity o) -tuples_on A); definition let U0 be Universal_Algebra; let A be non empty Subset of U0; func Opers (U0,A) -> PFuncFinSequence of A means :Def6: :: UNIALG_2:def 6 ( dom it = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom it & o = the charact of U0 . n holds it . n = o /. A ) ); existence ex b1 being PFuncFinSequence of A st ( dom b1 = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom b1 & o = the charact of U0 . n holds b1 . n = o /. A ) ) proof defpred S1[ Nat, set ] means for o being operation of U0 st o = the charact of U0 . \$1 holds \$2 = o /. A; A1: for n being Nat st n in Seg (len the charact of U0) holds ex x being Element of PFuncs ((A *),A) st S1[n,x] proof let n be Nat; ::_thesis: ( n in Seg (len the charact of U0) implies ex x being Element of PFuncs ((A *),A) st S1[n,x] ) assume n in Seg (len the charact of U0) ; ::_thesis: ex x being Element of PFuncs ((A *),A) st S1[n,x] then n in dom the charact of U0 by FINSEQ_1:def_3; then reconsider o1 = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; reconsider x = o1 /. A as Element of PFuncs ((A *),A) by PARTFUN1:45; take x ; ::_thesis: S1[n,x] let o be operation of U0; ::_thesis: ( o = the charact of U0 . n implies x = o /. A ) assume o = the charact of U0 . n ; ::_thesis: x = o /. A hence x = o /. A ; ::_thesis: verum end; consider p being FinSequence of PFuncs ((A *),A) such that A2: dom p = Seg (len the charact of U0) and A3: for n being Nat st n in Seg (len the charact of U0) holds S1[n,p . n] from FINSEQ_1:sch_5(A1); reconsider p = p as PFuncFinSequence of A ; take p ; ::_thesis: ( dom p = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom p & o = the charact of U0 . n holds p . n = o /. A ) ) thus dom p = dom the charact of U0 by A2, FINSEQ_1:def_3; ::_thesis: for n being set for o being operation of U0 st n in dom p & o = the charact of U0 . n holds p . n = o /. A let n be set ; ::_thesis: for o being operation of U0 st n in dom p & o = the charact of U0 . n holds p . n = o /. A let o be operation of U0; ::_thesis: ( n in dom p & o = the charact of U0 . n implies p . n = o /. A ) assume ( n in dom p & o = the charact of U0 . n ) ; ::_thesis: p . n = o /. A hence p . n = o /. A by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being PFuncFinSequence of A st dom b1 = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom b1 & o = the charact of U0 . n holds b1 . n = o /. A ) & dom b2 = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom b2 & o = the charact of U0 . n holds b2 . n = o /. A ) holds b1 = b2 proof let p1, p2 be PFuncFinSequence of A; ::_thesis: ( dom p1 = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds p1 . n = o /. A ) & dom p2 = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds p2 . n = o /. A ) implies p1 = p2 ) assume that A4: dom p1 = dom the charact of U0 and A5: for n being set for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds p1 . n = o /. A and A6: dom p2 = dom the charact of U0 and A7: for n being set for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds p2 . n = o /. A ; ::_thesis: p1 = p2 for n being Nat st n in dom the charact of U0 holds p1 . n = p2 . n proof let n be Nat; ::_thesis: ( n in dom the charact of U0 implies p1 . n = p2 . n ) assume A8: n in dom the charact of U0 ; ::_thesis: p1 . n = p2 . n then reconsider k = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; p1 . n = k /. A by A4, A5, A8; hence p1 . n = p2 . n by A6, A7, A8; ::_thesis: verum end; hence p1 = p2 by A4, A6, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def6 defines Opers UNIALG_2:def_6_:_ for U0 being Universal_Algebra for A being non empty Subset of U0 for b3 being PFuncFinSequence of A holds ( b3 = Opers (U0,A) iff ( dom b3 = dom the charact of U0 & ( for n being set for o being operation of U0 st n in dom b3 & o = the charact of U0 . n holds b3 . n = o /. A ) ) ); theorem Th4: :: UNIALG_2:4 for U0 being Universal_Algebra for B being non empty Subset of U0 st B = the carrier of U0 holds ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) proof let U0 be Universal_Algebra; ::_thesis: for B being non empty Subset of U0 st B = the carrier of U0 holds ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) let B be non empty Subset of U0; ::_thesis: ( B = the carrier of U0 implies ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) ) assume A1: B = the carrier of U0 ; ::_thesis: ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) A2: for o being operation of U0 holds B is_closed_on o proof let o be operation of U0; ::_thesis: B is_closed_on o let s be FinSequence of B; :: according to UNIALG_2:def_3 ::_thesis: ( len s = arity o implies o . s in B ) assume A3: len s = arity o ; ::_thesis: o . s in B ( dom o = (arity o) -tuples_on B & s is Element of (len s) -tuples_on B ) by A1, FINSEQ_2:92, MARGREL1:22; then A4: o . s in rng o by A3, FUNCT_1:def_3; rng o c= B by A1, RELAT_1:def_19; hence o . s in B by A4; ::_thesis: verum end; for o being operation of U0 holds o /. B = o proof let o be operation of U0; ::_thesis: o /. B = o ( dom o = (arity o) -tuples_on B & o /. B = o | ((arity o) -tuples_on B) ) by A1, A2, Def5, MARGREL1:22; hence o /. B = o by RELAT_1:68; ::_thesis: verum end; hence ( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) ) by A2, Def4; ::_thesis: verum end; theorem :: UNIALG_2:5 for U1 being Universal_Algebra for A being non empty Subset of U1 for o being operation of U1 st A is_closed_on o holds arity (o /. A) = arity o proof let U1 be Universal_Algebra; ::_thesis: for A being non empty Subset of U1 for o being operation of U1 st A is_closed_on o holds arity (o /. A) = arity o let A be non empty Subset of U1; ::_thesis: for o being operation of U1 st A is_closed_on o holds arity (o /. A) = arity o let o be operation of U1; ::_thesis: ( A is_closed_on o implies arity (o /. A) = arity o ) assume A is_closed_on o ; ::_thesis: arity (o /. A) = arity o then o /. A = o | ((arity o) -tuples_on A) by Def5; then dom (o /. A) = (dom o) /\ ((arity o) -tuples_on A) by RELAT_1:61; then A1: dom (o /. A) = ((arity o) -tuples_on the carrier of U1) /\ ((arity o) -tuples_on A) by MARGREL1:22 .= (arity o) -tuples_on A by MARGREL1:21 ; dom (o /. A) = (arity (o /. A)) -tuples_on A by MARGREL1:22; hence arity (o /. A) = arity o by A1, FINSEQ_2:110; ::_thesis: verum end; definition let U0 be Universal_Algebra; mode SubAlgebra of U0 -> Universal_Algebra means :Def7: :: UNIALG_2:def 7 ( the carrier of it is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of it holds ( the charact of it = Opers (U0,B) & B is opers_closed ) ) ); existence ex b1 being Universal_Algebra st ( the carrier of b1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b1 holds ( the charact of b1 = Opers (U0,B) & B is opers_closed ) ) ) proof take U1 = U0; ::_thesis: ( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds ( the charact of U1 = Opers (U0,B) & B is opers_closed ) ) ) A1: for B being non empty Subset of U0 st B = the carrier of U0 holds ( the charact of U0 = Opers (U0,B) & B is opers_closed ) proof let B be non empty Subset of U0; ::_thesis: ( B = the carrier of U0 implies ( the charact of U0 = Opers (U0,B) & B is opers_closed ) ) assume A2: B = the carrier of U0 ; ::_thesis: ( the charact of U0 = Opers (U0,B) & B is opers_closed ) A3: dom the charact of U0 = dom (Opers (U0,B)) by Def6; for n being Nat st n in dom the charact of U0 holds the charact of U0 . n = (Opers (U0,B)) . n proof let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of U0 . n = (Opers (U0,B)) . n ) assume A4: n in dom the charact of U0 ; ::_thesis: the charact of U0 . n = (Opers (U0,B)) . n then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; (Opers (U0,B)) . n = o /. B by A3, A4, Def6; hence the charact of U0 . n = (Opers (U0,B)) . n by A2, Th4; ::_thesis: verum end; hence ( the charact of U0 = Opers (U0,B) & B is opers_closed ) by A2, A3, Th4, FINSEQ_1:13; ::_thesis: verum end; the carrier of U1 c= the carrier of U1 ; hence ( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds ( the charact of U1 = Opers (U0,B) & B is opers_closed ) ) ) by A1; ::_thesis: verum end; end; :: deftheorem Def7 defines SubAlgebra UNIALG_2:def_7_:_ for U0, b2 being Universal_Algebra holds ( b2 is SubAlgebra of U0 iff ( the carrier of b2 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b2 holds ( the charact of b2 = Opers (U0,B) & B is opers_closed ) ) ) ); registration let U0 be Universal_Algebra; cluster non empty strict V84() quasi_total non-empty for SubAlgebra of U0; existence ex b1 being SubAlgebra of U0 st b1 is strict proof reconsider S = UAStr(# the carrier of U0, the charact of U0 #) as strict Universal_Algebra by UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; A1: the carrier of S c= the carrier of U0 ; for B being non empty Subset of U0 st B = the carrier of S holds ( the charact of S = Opers (U0,B) & B is opers_closed ) proof let B be non empty Subset of U0; ::_thesis: ( B = the carrier of S implies ( the charact of S = Opers (U0,B) & B is opers_closed ) ) assume A2: B = the carrier of S ; ::_thesis: ( the charact of S = Opers (U0,B) & B is opers_closed ) A3: now__::_thesis:_for_n_being_Nat_st_n_in_dom_the_charact_of_U0_holds_ (Opers_(U0,B))_._n_=_the_charact_of_U0_._n let n be Nat; ::_thesis: ( n in dom the charact of U0 implies (Opers (U0,B)) . n = the charact of U0 . n ) assume A4: n in dom the charact of U0 ; ::_thesis: (Opers (U0,B)) . n = the charact of U0 . n then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; n in dom (Opers (U0,B)) by A4, Def6; hence (Opers (U0,B)) . n = o /. B by Def6 .= the charact of U0 . n by A2, Th4 ; ::_thesis: verum end; dom the charact of U0 = dom (Opers (U0,B)) by Def6; hence ( the charact of S = Opers (U0,B) & B is opers_closed ) by A2, A3, Th4, FINSEQ_1:13; ::_thesis: verum end; then reconsider S = S as SubAlgebra of U0 by A1, Def7; take S ; ::_thesis: S is strict thus S is strict ; ::_thesis: verum end; end; theorem Th6: :: UNIALG_2:6 for U0, U1 being Universal_Algebra for o0 being operation of U0 for o1 being operation of U1 for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds arity o0 = arity o1 proof let U0, U1 be Universal_Algebra; ::_thesis: for o0 being operation of U0 for o1 being operation of U1 for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds arity o0 = arity o1 let o0 be operation of U0; ::_thesis: for o1 being operation of U1 for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds arity o0 = arity o1 let o1 be operation of U1; ::_thesis: for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds arity o0 = arity o1 let n be Nat; ::_thesis: ( U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n implies arity o0 = arity o1 ) assume that A1: U0 is SubAlgebra of U1 and A2: ( n in dom the charact of U0 & o0 = the charact of U0 . n ) and A3: o1 = the charact of U1 . n ; ::_thesis: arity o0 = arity o1 reconsider A = the carrier of U0 as non empty Subset of U1 by A1, Def7; A is opers_closed by A1, Def7; then A4: A is_closed_on o1 by Def4; ( n in dom (Opers (U1,A)) & o0 = (Opers (U1,A)) . n ) by A1, A2, Def7; then o0 = o1 /. A by A3, Def6; then o0 = o1 | ((arity o1) -tuples_on A) by A4, Def5; then dom o0 = (dom o1) /\ ((arity o1) -tuples_on A) by RELAT_1:61; then A5: dom o0 = ((arity o1) -tuples_on the carrier of U1) /\ ((arity o1) -tuples_on A) by MARGREL1:22 .= (arity o1) -tuples_on A by MARGREL1:21 ; dom o0 = (arity o0) -tuples_on A by MARGREL1:22; hence arity o0 = arity o1 by A5, FINSEQ_2:110; ::_thesis: verum end; theorem Th7: :: UNIALG_2:7 for U0, U1 being Universal_Algebra st U0 is SubAlgebra of U1 holds dom the charact of U0 = dom the charact of U1 proof let U0, U1 be Universal_Algebra; ::_thesis: ( U0 is SubAlgebra of U1 implies dom the charact of U0 = dom the charact of U1 ) assume A1: U0 is SubAlgebra of U1 ; ::_thesis: dom the charact of U0 = dom the charact of U1 then reconsider A = the carrier of U0 as non empty Subset of U1 by Def7; the charact of U0 = Opers (U1,A) by A1, Def7; hence dom the charact of U0 = dom the charact of U1 by Def6; ::_thesis: verum end; theorem :: UNIALG_2:8 for U0 being Universal_Algebra holds U0 is SubAlgebra of U0 proof let U0 be Universal_Algebra; ::_thesis: U0 is SubAlgebra of U0 A1: for B being non empty Subset of U0 st B = the carrier of U0 holds ( the charact of U0 = Opers (U0,B) & B is opers_closed ) proof let B be non empty Subset of U0; ::_thesis: ( B = the carrier of U0 implies ( the charact of U0 = Opers (U0,B) & B is opers_closed ) ) assume A2: B = the carrier of U0 ; ::_thesis: ( the charact of U0 = Opers (U0,B) & B is opers_closed ) A3: dom the charact of U0 = dom (Opers (U0,B)) by Def6; for n being Nat st n in dom the charact of U0 holds the charact of U0 . n = (Opers (U0,B)) . n proof let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of U0 . n = (Opers (U0,B)) . n ) assume A4: n in dom the charact of U0 ; ::_thesis: the charact of U0 . n = (Opers (U0,B)) . n then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; (Opers (U0,B)) . n = o /. B by A3, A4, Def6; hence the charact of U0 . n = (Opers (U0,B)) . n by A2, Th4; ::_thesis: verum end; hence ( the charact of U0 = Opers (U0,B) & B is opers_closed ) by A2, A3, Th4, FINSEQ_1:13; ::_thesis: verum end; the carrier of U0 c= the carrier of U0 ; hence U0 is SubAlgebra of U0 by A1, Def7; ::_thesis: verum end; theorem :: UNIALG_2:9 for U0, U1, U2 being Universal_Algebra st U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 holds U0 is SubAlgebra of U2 proof let U0, U1, U2 be Universal_Algebra; ::_thesis: ( U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of U2 ) assume that A1: U0 is SubAlgebra of U1 and A2: U1 is SubAlgebra of U2 ; ::_thesis: U0 is SubAlgebra of U2 A3: the carrier of U0 is Subset of U1 by A1, Def7; reconsider B2 = the carrier of U1 as non empty Subset of U2 by A2, Def7; A4: the charact of U1 = Opers (U2,B2) by A2, Def7; the carrier of U1 is Subset of U2 by A2, Def7; hence the carrier of U0 is Subset of U2 by A3, XBOOLE_1:1; :: according to UNIALG_2:def_7 ::_thesis: for B being non empty Subset of U2 st B = the carrier of U0 holds ( the charact of U0 = Opers (U2,B) & B is opers_closed ) let B be non empty Subset of U2; ::_thesis: ( B = the carrier of U0 implies ( the charact of U0 = Opers (U2,B) & B is opers_closed ) ) assume A5: B = the carrier of U0 ; ::_thesis: ( the charact of U0 = Opers (U2,B) & B is opers_closed ) reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1, Def7; A6: the charact of U0 = Opers (U1,B1) by A1, Def7; A7: B2 is opers_closed by A2, Def7; A8: dom the charact of U1 = dom (Opers (U2,B2)) by A2, Def7 .= dom the charact of U2 by Def6 ; A9: B1 is opers_closed by A1, Def7; A10: now__::_thesis:_for_o2_being_operation_of_U2_holds_B_is_closed_on_o2 let o2 be operation of U2; ::_thesis: B is_closed_on o2 consider n being Nat such that A11: n in dom the charact of U2 and A12: the charact of U2 . n = o2 by FINSEQ_2:10; A13: dom the charact of U2 = dom (Opers (U2,B2)) by Def6; then reconsider o21 = the charact of U1 . n as operation of U1 by A4, A11, FUNCT_1:def_3; A14: dom o21 = (arity o21) -tuples_on the carrier of U1 by MARGREL1:22; A15: dom the charact of U1 = dom (Opers (U1,B1)) by Def6; then reconsider o20 = the charact of U0 . n as operation of U0 by A6, A4, A11, A13, FUNCT_1:def_3; A16: dom o20 = (arity o20) -tuples_on the carrier of U0 by MARGREL1:22; A17: ( dom o2 = (arity o2) -tuples_on the carrier of U2 & dom (o2 | ((arity o2) -tuples_on B2)) = (dom o2) /\ ((arity o2) -tuples_on B2) ) by MARGREL1:22, RELAT_1:61; A18: B2 is_closed_on o2 by A7, Def4; A19: o21 = o2 /. B2 by A4, A11, A12, A13, Def6; then o21 = o2 | ((arity o2) -tuples_on B2) by A18, Def5; then A20: arity o2 = arity o21 by A14, A17, FINSEQ_2:110, MARGREL1:21; A21: B1 is_closed_on o21 by A9, Def4; A22: o20 = o21 /. B1 by A6, A4, A11, A13, A15, Def6; then o20 = o21 | ((arity o21) -tuples_on B1) by A21, Def5; then (arity o20) -tuples_on B1 = ((arity o21) -tuples_on the carrier of U1) /\ ((arity o21) -tuples_on B1) by A16, A14, RELAT_1:61; then A23: arity o20 = arity o21 by FINSEQ_2:110, MARGREL1:21; now__::_thesis:_for_s_being_FinSequence_of_B_st_len_s_=_arity_o2_holds_ o2_._s_in_B let s be FinSequence of B; ::_thesis: ( len s = arity o2 implies o2 . s in B ) reconsider s1 = s as Element of B1 * by A5, FINSEQ_1:def_11; reconsider s0 = s as Element of the carrier of U0 * by A5, FINSEQ_1:def_11; A24: rng o20 c= B by A5, RELAT_1:def_19; rng s c= B by FINSEQ_1:def_4; then rng s c= B2 by A3, A5, XBOOLE_1:1; then s is FinSequence of B2 by FINSEQ_1:def_4; then reconsider s2 = s as Element of B2 * by FINSEQ_1:def_11; assume A25: len s = arity o2 ; ::_thesis: o2 . s in B then s2 in { w where w is Element of B2 * : len w = arity o2 } ; then A26: s2 in (arity o2) -tuples_on B2 by FINSEQ_2:def_4; s0 in { w where w is Element of the carrier of U0 * : len w = arity o20 } by A23, A20, A25; then s0 in (arity o20) -tuples_on the carrier of U0 by FINSEQ_2:def_4; then A27: o20 . s0 in rng o20 by A16, FUNCT_1:def_3; s1 in { w where w is Element of B1 * : len w = arity o21 } by A20, A25; then A28: s1 in (arity o21) -tuples_on B1 by FINSEQ_2:def_4; o20 . s0 = (o21 | ((arity o21) -tuples_on B1)) . s1 by A21, A22, Def5 .= o21 . s1 by A28, FUNCT_1:49 .= (o2 | ((arity o2) -tuples_on B2)) . s2 by A18, A19, Def5 .= o2 . s by A26, FUNCT_1:49 ; hence o2 . s in B by A27, A24; ::_thesis: verum end; hence B is_closed_on o2 by Def3; ::_thesis: verum end; A29: dom the charact of U0 = dom (Opers (U1,B1)) by A1, Def7 .= dom the charact of U1 by Def6 ; A30: dom the charact of U2 = dom (Opers (U2,B)) by Def6; A31: B = B1 by A5; now__::_thesis:_for_n_being_Nat_st_n_in_dom_(Opers_(U2,B))_holds_ (Opers_(U2,B))_._n_=_the_charact_of_U0_._n let n be Nat; ::_thesis: ( n in dom (Opers (U2,B)) implies (Opers (U2,B)) . n = the charact of U0 . n ) assume A32: n in dom (Opers (U2,B)) ; ::_thesis: (Opers (U2,B)) . n = the charact of U0 . n then reconsider o2 = the charact of U2 . n as operation of U2 by A30, FUNCT_1:def_3; reconsider o21 = the charact of U1 . n as operation of U1 by A8, A30, A32, FUNCT_1:def_3; A33: B2 is_closed_on o2 by A7, Def4; A34: B1 is_closed_on o21 by A9, Def4; thus (Opers (U2,B)) . n = o2 /. B by A32, Def6 .= o2 | ((arity o2) -tuples_on B) by A10, Def5 .= o2 | (((arity o2) -tuples_on B2) /\ ((arity o2) -tuples_on B)) by A31, MARGREL1:21 .= (o2 | ((arity o2) -tuples_on B2)) | ((arity o2) -tuples_on B) by RELAT_1:71 .= (o2 /. B2) | ((arity o2) -tuples_on B) by A33, Def5 .= o21 | ((arity o2) -tuples_on B) by A4, A8, A30, A32, Def6 .= o21 | ((arity o21) -tuples_on B1) by A2, A5, A8, A30, A32, Th6 .= o21 /. B1 by A34, Def5 .= the charact of U0 . n by A6, A29, A8, A30, A32, Def6 ; ::_thesis: verum end; hence the charact of U0 = Opers (U2,B) by A29, A8, A30, FINSEQ_1:13; ::_thesis: B is opers_closed thus B is opers_closed by A10, Def4; ::_thesis: verum end; theorem Th10: :: UNIALG_2:10 for U1, U2 being Universal_Algebra st U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 holds U1 = U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2 ) assume that A1: U1 is strict SubAlgebra of U2 and A2: U2 is strict SubAlgebra of U1 ; ::_thesis: U1 = U2 reconsider B = the carrier of U1 as non empty Subset of U2 by A1, Def7; the carrier of U2 c= the carrier of U2 ; then reconsider B1 = the carrier of U2 as non empty Subset of U2 ; A3: dom (Opers (U2,B1)) = dom the charact of U2 by Def6; A4: for n being Nat st n in dom the charact of U2 holds the charact of U2 . n = (Opers (U2,B1)) . n proof let n be Nat; ::_thesis: ( n in dom the charact of U2 implies the charact of U2 . n = (Opers (U2,B1)) . n ) assume A5: n in dom the charact of U2 ; ::_thesis: the charact of U2 . n = (Opers (U2,B1)) . n then reconsider o = the charact of U2 . n as operation of U2 by FUNCT_1:def_3; (Opers (U2,B1)) . n = o /. B1 by A3, A5, Def6 .= o by Th4 ; hence the charact of U2 . n = (Opers (U2,B1)) . n ; ::_thesis: verum end; the carrier of U2 is Subset of U1 by A2, Def7; then A6: B1 = B by XBOOLE_0:def_10; then the charact of U1 = Opers (U2,B1) by A1, Def7; hence U1 = U2 by A1, A2, A6, A3, A4, FINSEQ_1:13; ::_thesis: verum end; theorem Th11: :: UNIALG_2:11 for U0 being Universal_Algebra for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds U1 is SubAlgebra of U2 proof let U0 be Universal_Algebra; ::_thesis: for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds U1 is SubAlgebra of U2 let U1, U2 be SubAlgebra of U0; ::_thesis: ( the carrier of U1 c= the carrier of U2 implies U1 is SubAlgebra of U2 ) A1: dom the charact of U1 = dom the charact of U0 by Th7; reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7; assume A2: the carrier of U1 c= the carrier of U2 ; ::_thesis: U1 is SubAlgebra of U2 hence the carrier of U1 is Subset of U2 ; :: according to UNIALG_2:def_7 ::_thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds ( the charact of U1 = Opers (U2,B) & B is opers_closed ) let B be non empty Subset of U2; ::_thesis: ( B = the carrier of U1 implies ( the charact of U1 = Opers (U2,B) & B is opers_closed ) ) assume A3: B = the carrier of U1 ; ::_thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed ) reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7; A4: the charact of U2 = Opers (U0,B2) by Def7; A5: B2 is opers_closed by Def7; A6: dom (Opers (U2,B)) = dom the charact of U2 by Def6; A7: dom the charact of U2 = dom the charact of U0 by Th7; A8: B1 is opers_closed by Def7; A9: B is opers_closed proof let o2 be operation of U2; :: according to UNIALG_2:def_4 ::_thesis: B is_closed_on o2 let s be FinSequence of B; :: according to UNIALG_2:def_3 ::_thesis: ( len s = arity o2 implies o2 . s in B ) consider n being Nat such that A10: n in dom the charact of U2 and A11: the charact of U2 . n = o2 by FINSEQ_2:10; reconsider o0 = the charact of U0 . n as operation of U0 by A7, A10, FUNCT_1:def_3; A12: arity o2 = arity o0 by A10, A11, Th6; rng s c= B by FINSEQ_1:def_4; then rng s c= B2 by XBOOLE_1:1; then s is FinSequence of B2 by FINSEQ_1:def_4; then reconsider s2 = s as Element of B2 * by FINSEQ_1:def_11; reconsider s1 = s as Element of B1 * by A3, FINSEQ_1:def_11; assume A13: arity o2 = len s ; ::_thesis: o2 . s in B set tb2 = (arity o0) -tuples_on B2; A14: B2 is_closed_on o0 by A5, Def4; A15: o2 = o0 /. B2 by A4, A10, A11, Def6 .= o0 | ((arity o0) -tuples_on B2) by A14, Def5 ; A16: B1 is_closed_on o0 by A8, Def4; (arity o0) -tuples_on B2 = { w where w is Element of B2 * : len w = arity o0 } by FINSEQ_2:def_4; then s2 in (arity o0) -tuples_on B2 by A13, A12; then o2 . s = o0 . s1 by A15, FUNCT_1:49; hence o2 . s in B by A3, A13, A16, A12, Def3; ::_thesis: verum end; A17: the charact of U1 = Opers (U0,B1) by Def7; now__::_thesis:_for_n_being_Nat_st_n_in_dom_the_charact_of_U0_holds_ the_charact_of_U1_._n_=_(Opers_(U2,B))_._n let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of U1 . n = (Opers (U2,B)) . n ) assume A18: n in dom the charact of U0 ; ::_thesis: the charact of U1 . n = (Opers (U2,B)) . n then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; reconsider o2 = the charact of U2 . n as operation of U2 by A7, A18, FUNCT_1:def_3; A19: ( o2 = o0 /. B2 & arity o2 = arity o0 ) by A4, A7, A18, Def6, Th6; A20: B is_closed_on o2 by A9, Def4; A21: B2 is_closed_on o0 by A5, Def4; A22: B1 is_closed_on o0 by A8, Def4; thus the charact of U1 . n = o0 /. B1 by A17, A1, A18, Def6 .= o0 | ((arity o0) -tuples_on B1) by A22, Def5 .= o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1)) by A2, MARGREL1:21 .= (o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B) by A3, RELAT_1:71 .= (o0 /. B2) | ((arity o0) -tuples_on B) by A21, Def5 .= o2 /. B by A20, A19, Def5 .= (Opers (U2,B)) . n by A7, A6, A18, Def6 ; ::_thesis: verum end; hence the charact of U1 = Opers (U2,B) by A1, A7, A6, FINSEQ_1:13; ::_thesis: B is opers_closed thus B is opers_closed by A9; ::_thesis: verum end; theorem Th12: :: UNIALG_2:12 for U0 being Universal_Algebra for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds U1 = U2 proof let U0 be Universal_Algebra; ::_thesis: for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds U1 = U2 let U1, U2 be strict SubAlgebra of U0; ::_thesis: ( the carrier of U1 = the carrier of U2 implies U1 = U2 ) assume the carrier of U1 = the carrier of U2 ; ::_thesis: U1 = U2 then ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 ) by Th11; hence U1 = U2 by Th10; ::_thesis: verum end; theorem :: UNIALG_2:13 for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds U1,U2 are_similar proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 implies U1,U2 are_similar ) set s1 = signature U1; set s2 = signature U2; set X = dom (signature U1); len (signature U1) = len the charact of U1 by UNIALG_1:def_4; then A1: dom (signature U1) = dom the charact of U1 by FINSEQ_3:29; assume A2: U1 is SubAlgebra of U2 ; ::_thesis: U1,U2 are_similar then reconsider A = the carrier of U1 as non empty Subset of U2 by Def7; len (signature U2) = len the charact of U2 by UNIALG_1:def_4; then A3: dom (signature U2) = dom the charact of U2 by FINSEQ_3:29; dom the charact of U1 = dom (Opers (U2,A)) by A2, Def7; then A4: dom (signature U1) = dom (signature U2) by A1, A3, Def6; the charact of U1 = Opers (U2,A) by A2, Def7; then A5: dom (signature U1) c= dom (signature U2) by A1, A3, Def6; for n being Nat st n in dom (signature U1) holds (signature U1) . n = (signature U2) . n proof let n be Nat; ::_thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature U2) . n ) assume A6: n in dom (signature U1) ; ::_thesis: (signature U1) . n = (signature U2) . n then reconsider o1 = the charact of U1 . n as operation of U1 by A1, FUNCT_1:def_3; reconsider o2 = the charact of U2 . n as operation of U2 by A3, A4, A6, FUNCT_1:def_3; ( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A5, A6, UNIALG_1:def_4; hence (signature U1) . n = (signature U2) . n by A2, A1, A6, Th6; ::_thesis: verum end; then signature U1 = signature U2 by A4, FINSEQ_1:13; hence U1,U2 are_similar by Def1; ::_thesis: verum end; theorem Th14: :: UNIALG_2:14 for U0 being Universal_Algebra for A being non empty Subset of U0 holds UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra proof let U0 be Universal_Algebra; ::_thesis: for A being non empty Subset of U0 holds UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra let A be non empty Subset of U0; ::_thesis: UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra set C = UAStr(# A,(Opers (U0,A)) #); A1: dom the charact of UAStr(# A,(Opers (U0,A)) #) = dom the charact of U0 by Def6; for n being set st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) holds not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty proof let n be set ; ::_thesis: ( n in dom the charact of UAStr(# A,(Opers (U0,A)) #) implies not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty ) assume A2: n in dom the charact of UAStr(# A,(Opers (U0,A)) #) ; ::_thesis: not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty then reconsider o = the charact of U0 . n as operation of U0 by A1, FUNCT_1:def_3; the charact of UAStr(# A,(Opers (U0,A)) #) . n = o /. A by A2, Def6; hence not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty ; ::_thesis: verum end; then A3: the charact of UAStr(# A,(Opers (U0,A)) #) is non-empty by FUNCT_1:def_9; for n being Nat for h being PartFunc of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds h is quasi_total proof let n be Nat; ::_thesis: for h being PartFunc of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds h is quasi_total let h be PartFunc of ( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the carrier of UAStr(# A,(Opers (U0,A)) #); ::_thesis: ( n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n implies h is quasi_total ) assume that A4: n in dom the charact of UAStr(# A,(Opers (U0,A)) #) and A5: h = the charact of UAStr(# A,(Opers (U0,A)) #) . n ; ::_thesis: h is quasi_total reconsider o = the charact of U0 . n as operation of U0 by A1, A4, FUNCT_1:def_3; h = o /. A by A4, A5, Def6; hence h is quasi_total ; ::_thesis: verum end; then A6: the charact of UAStr(# A,(Opers (U0,A)) #) is quasi_total by MARGREL1:def_24; for n being Nat for h being PartFunc of ( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the carrier of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds h is homogeneous proof let n be Nat; ::_thesis: for h being PartFunc of ( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the carrier of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds h is homogeneous let h be PartFunc of ( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the carrier of UAStr(# A,(Opers (U0,A)) #); ::_thesis: ( n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n implies h is homogeneous ) assume that A7: n in dom the charact of UAStr(# A,(Opers (U0,A)) #) and A8: h = the charact of UAStr(# A,(Opers (U0,A)) #) . n ; ::_thesis: h is homogeneous reconsider o = the charact of U0 . n as operation of U0 by A1, A7, FUNCT_1:def_3; h = o /. A by A7, A8, Def6; hence h is homogeneous ; ::_thesis: verum end; then A9: the charact of UAStr(# A,(Opers (U0,A)) #) is homogeneous by MARGREL1:def_23; the charact of UAStr(# A,(Opers (U0,A)) #) <> {} by A1, RELAT_1:38, RELAT_1:41; hence UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra by A9, A6, A3, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum end; definition let U0 be Universal_Algebra; let A be non empty Subset of U0; assume A1: A is opers_closed ; func UniAlgSetClosed A -> strict SubAlgebra of U0 equals :Def8: :: UNIALG_2:def 8 UAStr(# A,(Opers (U0,A)) #); coherence UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0 proof reconsider C = UAStr(# A,(Opers (U0,A)) #) as strict Universal_Algebra by Th14; for B being non empty Subset of U0 st B = the carrier of C holds ( the charact of C = Opers (U0,B) & B is opers_closed ) by A1; hence UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0 by Def7; ::_thesis: verum end; end; :: deftheorem Def8 defines UniAlgSetClosed UNIALG_2:def_8_:_ for U0 being Universal_Algebra for A being non empty Subset of U0 st A is opers_closed holds UniAlgSetClosed A = UAStr(# A,(Opers (U0,A)) #); definition let U0 be Universal_Algebra; let U1, U2 be SubAlgebra of U0; assume A1: the carrier of U1 meets the carrier of U2 ; funcU1 /\ U2 -> strict SubAlgebra of U0 means :Def9: :: UNIALG_2:def 9 ( the carrier of it = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of it holds ( the charact of it = Opers (U0,B) & B is opers_closed ) ) ); existence ex b1 being strict SubAlgebra of U0 st ( the carrier of b1 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b1 holds ( the charact of b1 = Opers (U0,B) & B is opers_closed ) ) ) proof A2: the carrier of U1 /\ the carrier of U2 c= the carrier of U1 by XBOOLE_1:17; the carrier of U1 is Subset of U0 by Def7; then reconsider C = the carrier of U1 /\ the carrier of U2 as non empty Subset of U0 by A1, A2, XBOOLE_0:def_7, XBOOLE_1:1; set S = UAStr(# C,(Opers (U0,C)) #); A3: the carrier of U1 /\ the carrier of U2 c= the carrier of U2 by XBOOLE_1:17; A4: now__::_thesis:_for_o_being_operation_of_U0_holds_C_is_closed_on_o let o be operation of U0; ::_thesis: C is_closed_on o now__::_thesis:_for_s_being_FinSequence_of_C_st_len_s_=_arity_o_holds_ o_._s_in_C set B1 = the carrier of U1; set B2 = the carrier of U2; let s be FinSequence of C; ::_thesis: ( len s = arity o implies o . s in C ) reconsider s2 = s as FinSequence of the carrier of U2 by A3, FINSEQ_2:24; reconsider s1 = s as FinSequence of the carrier of U1 by A2, FINSEQ_2:24; assume A5: len s = arity o ; ::_thesis: o . s in C reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7; reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7; B2 is opers_closed by Def7; then B2 is_closed_on o by Def4; then A6: o . s2 in B2 by A5, Def3; B1 is opers_closed by Def7; then B1 is_closed_on o by Def4; then o . s1 in B1 by A5, Def3; hence o . s in C by A6, XBOOLE_0:def_4; ::_thesis: verum end; hence C is_closed_on o by Def3; ::_thesis: verum end; then A7: for B being non empty Subset of U0 st B = the carrier of UAStr(# C,(Opers (U0,C)) #) holds ( the charact of UAStr(# C,(Opers (U0,C)) #) = Opers (U0,B) & B is opers_closed ) by Def4; reconsider S = UAStr(# C,(Opers (U0,C)) #) as Universal_Algebra by Th14; reconsider S = S as strict SubAlgebra of U0 by A7, Def7; take S ; ::_thesis: ( the carrier of S = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of S holds ( the charact of S = Opers (U0,B) & B is opers_closed ) ) ) thus ( the carrier of S = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of S holds ( the charact of S = Opers (U0,B) & B is opers_closed ) ) ) by A4, Def4; ::_thesis: verum end; uniqueness for b1, b2 being strict SubAlgebra of U0 st the carrier of b1 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b1 holds ( the charact of b1 = Opers (U0,B) & B is opers_closed ) ) & the carrier of b2 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b2 holds ( the charact of b2 = Opers (U0,B) & B is opers_closed ) ) holds b1 = b2 proof ( the carrier of U1 is Subset of U0 & the carrier of U1 /\ the carrier of U2 c= the carrier of U1 ) by Def7, XBOOLE_1:17; then reconsider C = the carrier of U1 /\ the carrier of U2 as non empty Subset of U0 by A1, XBOOLE_0:def_7, XBOOLE_1:1; let W1, W2 be strict SubAlgebra of U0; ::_thesis: ( the carrier of W1 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of W1 holds ( the charact of W1 = Opers (U0,B) & B is opers_closed ) ) & the carrier of W2 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of W2 holds ( the charact of W2 = Opers (U0,B) & B is opers_closed ) ) implies W1 = W2 ) assume that A8: ( the carrier of W1 = the carrier of U1 /\ the carrier of U2 & ( for B1 being non empty Subset of U0 st B1 = the carrier of W1 holds ( the charact of W1 = Opers (U0,B1) & B1 is opers_closed ) ) ) and A9: the carrier of W2 = the carrier of U1 /\ the carrier of U2 and A10: for B2 being non empty Subset of U0 st B2 = the carrier of W2 holds ( the charact of W2 = Opers (U0,B2) & B2 is opers_closed ) ; ::_thesis: W1 = W2 the charact of W2 = Opers (U0,C) by A9, A10; hence W1 = W2 by A8, A9; ::_thesis: verum end; end; :: deftheorem Def9 defines /\ UNIALG_2:def_9_:_ for U0 being Universal_Algebra for U1, U2 being SubAlgebra of U0 st the carrier of U1 meets the carrier of U2 holds for b4 being strict SubAlgebra of U0 holds ( b4 = U1 /\ U2 iff ( the carrier of b4 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b4 holds ( the charact of b4 = Opers (U0,B) & B is opers_closed ) ) ) ); definition let U0 be Universal_Algebra; func Constants U0 -> Subset of U0 equals :: UNIALG_2:def 10 { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } ; coherence { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } is Subset of U0 proof set E = { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } ; { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } c= the carrier of U0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } or x in the carrier of U0 ) assume x in { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } ; ::_thesis: x in the carrier of U0 then ex w being Element of U0 st ( w = x & ex o being operation of U0 st ( arity o = 0 & w in rng o ) ) ; hence x in the carrier of U0 ; ::_thesis: verum end; hence { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } is Subset of U0 ; ::_thesis: verum end; end; :: deftheorem defines Constants UNIALG_2:def_10_:_ for U0 being Universal_Algebra holds Constants U0 = { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } ; definition let IT be Universal_Algebra; attrIT is with_const_op means :Def11: :: UNIALG_2:def 11 ex o being operation of IT st arity o = 0 ; end; :: deftheorem Def11 defines with_const_op UNIALG_2:def_11_:_ for IT being Universal_Algebra holds ( IT is with_const_op iff ex o being operation of IT st arity o = 0 ); registration cluster non empty strict V84() quasi_total non-empty with_const_op for UAStr ; existence ex b1 being Universal_Algebra st ( b1 is with_const_op & b1 is strict ) proof set A = the non empty set ; set a = the Element of the non empty set ; reconsider w = (<*> the non empty set ) .--> the Element of the non empty set as Element of PFuncs (( the non empty set *), the non empty set ) by MARGREL1:19; set U0 = UAStr(# the non empty set ,<*w*> #); A1: ( the charact of UAStr(# the non empty set ,<*w*> #) is quasi_total & the charact of UAStr(# the non empty set ,<*w*> #) is homogeneous ) by MARGREL1:20; the charact of UAStr(# the non empty set ,<*w*> #) is non-empty by MARGREL1:20; then reconsider U0 = UAStr(# the non empty set ,<*w*> #) as Universal_Algebra by A1, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; take U0 ; ::_thesis: ( U0 is with_const_op & U0 is strict ) ( dom <*w*> = {1} & 1 in {1} ) by FINSEQ_1:2, FINSEQ_1:38, TARSKI:def_1; then reconsider o = the charact of U0 . 1 as operation of U0 by FUNCT_1:def_3; o = w by FINSEQ_1:40; then A2: dom o = {(<*> the non empty set )} by FUNCOP_1:13; A3: now__::_thesis:_for_x_being_FinSequence_st_x_in_dom_o_holds_ len_x_=_0 let x be FinSequence; ::_thesis: ( x in dom o implies len x = 0 ) assume x in dom o ; ::_thesis: len x = 0 then x = <*> the non empty set by A2, TARSKI:def_1; hence len x = 0 ; ::_thesis: verum end; <*> the non empty set in {(<*> the non empty set )} by TARSKI:def_1; then arity o = 0 by A2, A3, MARGREL1:def_25; hence ( U0 is with_const_op & U0 is strict ) by Def11; ::_thesis: verum end; end; registration let U0 be with_const_op Universal_Algebra; cluster Constants U0 -> non empty ; coherence not Constants U0 is empty proof consider o being operation of U0 such that A1: arity o = 0 by Def11; dom o = 0 -tuples_on the carrier of U0 by A1, MARGREL1:22 .= {(<*> the carrier of U0)} by FINSEQ_2:94 ; then <*> the carrier of U0 in dom o by TARSKI:def_1; then A2: o . (<*> the carrier of U0) in rng o by FUNCT_1:def_3; rng o c= the carrier of U0 by RELAT_1:def_19; then reconsider u = o . (<*> the carrier of U0) as Element of U0 by A2; u in { a where a is Element of U0 : ex o being operation of U0 st ( arity o = 0 & a in rng o ) } by A1, A2; hence not Constants U0 is empty ; ::_thesis: verum end; end; theorem Th15: :: UNIALG_2:15 for U0 being Universal_Algebra for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1 proof let U0 be Universal_Algebra; ::_thesis: for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1 let U1 be SubAlgebra of U0; ::_thesis: Constants U0 is Subset of U1 set u1 = the carrier of U1; Constants U0 c= the carrier of U1 proof reconsider B = the carrier of U1 as non empty Subset of U0 by Def7; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Constants U0 or x in the carrier of U1 ) assume x in Constants U0 ; ::_thesis: x in the carrier of U1 then consider a being Element of U0 such that A1: a = x and A2: ex o being operation of U0 st ( arity o = 0 & a in rng o ) ; consider o0 being operation of U0 such that A3: arity o0 = 0 and A4: a in rng o0 by A2; consider y being set such that A5: y in dom o0 and A6: a = o0 . y by A4, FUNCT_1:def_3; dom o0 = 0 -tuples_on the carrier of U0 by A3, MARGREL1:22 .= {(<*> the carrier of U0)} by FINSEQ_2:94 ; then y in {(<*> B)} by A5; then y in 0 -tuples_on B by FINSEQ_2:94; then y in (dom o0) /\ ((arity o0) -tuples_on B) by A3, A5, XBOOLE_0:def_4; then A7: y in dom (o0 | ((arity o0) -tuples_on B)) by RELAT_1:61; consider n being Nat such that A8: n in dom the charact of U0 and A9: the charact of U0 . n = o0 by FINSEQ_2:10; A10: n in dom the charact of U1 by A8, Th7; then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def_3; the charact of U1 = Opers (U0,B) by Def7; then A11: o1 = o0 /. B by A9, A10, Def6; B is opers_closed by Def7; then A12: B is_closed_on o0 by Def4; then y in dom (o0 /. B) by A7, Def5; then A13: o1 . y in rng o1 by A11, FUNCT_1:def_3; A14: rng o1 c= the carrier of U1 by RELAT_1:def_19; o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by A11, A12, Def5 .= a by A6, A7, FUNCT_1:47 ; hence x in the carrier of U1 by A1, A13, A14; ::_thesis: verum end; hence Constants U0 is Subset of U1 ; ::_thesis: verum end; theorem :: UNIALG_2:16 for U0 being with_const_op Universal_Algebra for U1 being SubAlgebra of U0 holds Constants U0 is non empty Subset of U1 by Th15; theorem Th17: :: UNIALG_2:17 for U0 being with_const_op Universal_Algebra for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2 proof let U0 be with_const_op Universal_Algebra; ::_thesis: for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2 let U1, U2 be SubAlgebra of U0; ::_thesis: the carrier of U1 meets the carrier of U2 set a = the Element of Constants U0; ( Constants U0 is non empty Subset of U1 & Constants U0 is non empty Subset of U2 ) by Th15; then A1: Constants U0 c= the carrier of U1 /\ the carrier of U2 by XBOOLE_1:19; the Element of Constants U0 in Constants U0 ; hence the carrier of U1 meets the carrier of U2 by A1, XBOOLE_0:4; ::_thesis: verum end; definition let U0 be Universal_Algebra; let A be Subset of U0; assume A1: ( Constants U0 <> {} or A <> {} ) ; func GenUnivAlg A -> strict SubAlgebra of U0 means :Def12: :: UNIALG_2:def 12 ( A c= the carrier of it & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds it is SubAlgebra of U1 ) ); existence ex b1 being strict SubAlgebra of U0 st ( A c= the carrier of b1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds b1 is SubAlgebra of U1 ) ) proof defpred S1[ set ] means ( A c= \$1 & Constants U0 c= \$1 & ( for B being non empty Subset of U0 st B = \$1 holds B is opers_closed ) ); set C = bool the carrier of U0; consider X being set such that A2: for x being set holds ( x in X iff ( x in bool the carrier of U0 & S1[x] ) ) from XBOOLE_0:sch_1(); set P = meet X; ( the carrier of U0 in bool the carrier of U0 & ( for B being non empty Subset of U0 st B = the carrier of U0 holds B is opers_closed ) ) by Th4, ZFMISC_1:def_1; then A3: the carrier of U0 in X by A2; A4: meet X c= the carrier of U0 proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in meet X or t in the carrier of U0 ) assume t in meet X ; ::_thesis: t in the carrier of U0 hence t in the carrier of U0 by A3, SETFAM_1:def_1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ A_\/_(Constants_U0)_c=_x let x be set ; ::_thesis: ( x in X implies A \/ (Constants U0) c= x ) assume x in X ; ::_thesis: A \/ (Constants U0) c= x then ( A c= x & Constants U0 c= x ) by A2; hence A \/ (Constants U0) c= x by XBOOLE_1:8; ::_thesis: verum end; then A5: A \/ (Constants U0) c= meet X by A3, SETFAM_1:5; then reconsider P = meet X as non empty Subset of U0 by A1, A4; take E = UniAlgSetClosed P; ::_thesis: ( A c= the carrier of E & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds E is SubAlgebra of U1 ) ) A6: P is opers_closed proof let o be operation of U0; :: according to UNIALG_2:def_4 ::_thesis: P is_closed_on o let s be FinSequence of P; :: according to UNIALG_2:def_3 ::_thesis: ( len s = arity o implies o . s in P ) assume A7: len s = arity o ; ::_thesis: o . s in P now__::_thesis:_for_a_being_set_st_a_in_X_holds_ o_._s_in_a let a be set ; ::_thesis: ( a in X implies o . s in a ) A8: rng s c= P by FINSEQ_1:def_4; assume A9: a in X ; ::_thesis: o . s in a then reconsider a0 = a as Subset of U0 by A2; ( A c= a0 & Constants U0 c= a0 ) by A2, A9; then reconsider a0 = a0 as non empty Subset of U0 by A1; P c= a0 by A9, SETFAM_1:3; then rng s c= a0 by A8, XBOOLE_1:1; then reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def_4; a0 is opers_closed by A2, A9; then a0 is_closed_on o by Def4; then o . s0 in a0 by A7, Def3; hence o . s in a ; ::_thesis: verum end; hence o . s in P by A3, SETFAM_1:def_1; ::_thesis: verum end; then A10: E = UAStr(# P,(Opers (U0,P)) #) by Def8; A c= A \/ (Constants U0) by XBOOLE_1:7; hence A c= the carrier of E by A5, A10, XBOOLE_1:1; ::_thesis: for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds E is SubAlgebra of U1 let U1 be SubAlgebra of U0; ::_thesis: ( A c= the carrier of U1 implies E is SubAlgebra of U1 ) assume A11: A c= the carrier of U1 ; ::_thesis: E is SubAlgebra of U1 set u1 = the carrier of U1; A12: Constants U0 c= the carrier of U1 proof reconsider B = the carrier of U1 as non empty Subset of U0 by Def7; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Constants U0 or x in the carrier of U1 ) assume x in Constants U0 ; ::_thesis: x in the carrier of U1 then consider a being Element of U0 such that A13: a = x and A14: ex o being operation of U0 st ( arity o = 0 & a in rng o ) ; consider o0 being operation of U0 such that A15: arity o0 = 0 and A16: a in rng o0 by A14; consider y being set such that A17: y in dom o0 and A18: a = o0 . y by A16, FUNCT_1:def_3; dom o0 = 0 -tuples_on the carrier of U0 by A15, MARGREL1:22 .= {(<*> the carrier of U0)} by FINSEQ_2:94 ; then y in {(<*> B)} by A17; then y in 0 -tuples_on B by FINSEQ_2:94; then y in (dom o0) /\ ((arity o0) -tuples_on B) by A15, A17, XBOOLE_0:def_4; then A19: y in dom (o0 | ((arity o0) -tuples_on B)) by RELAT_1:61; consider n being Nat such that A20: n in dom the charact of U0 and A21: the charact of U0 . n = o0 by FINSEQ_2:10; A22: n in dom the charact of U1 by A20, Th7; then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def_3; the charact of U1 = Opers (U0,B) by Def7; then A23: o1 = o0 /. B by A21, A22, Def6; B is opers_closed by Def7; then A24: B is_closed_on o0 by Def4; then y in dom (o0 /. B) by A19, Def5; then A25: o1 . y in rng o1 by A23, FUNCT_1:def_3; A26: rng o1 c= the carrier of U1 by RELAT_1:def_19; o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by A23, A24, Def5 .= a by A18, A19, FUNCT_1:47 ; hence x in the carrier of U1 by A13, A25, A26; ::_thesis: verum end; ( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds B is opers_closed ) ) by Def7; then A27: the carrier of U1 in X by A2, A11, A12; hence the carrier of E is Subset of U1 by A10, SETFAM_1:3; :: according to UNIALG_2:def_7 ::_thesis: for B being non empty Subset of U1 st B = the carrier of E holds ( the charact of E = Opers (U1,B) & B is opers_closed ) let B be non empty Subset of U1; ::_thesis: ( B = the carrier of E implies ( the charact of E = Opers (U1,B) & B is opers_closed ) ) assume A28: B = the carrier of E ; ::_thesis: ( the charact of E = Opers (U1,B) & B is opers_closed ) reconsider u11 = the carrier of U1 as non empty Subset of U0 by Def7; A29: the charact of U1 = Opers (U0,u11) by Def7; A30: dom the charact of U0 = dom (Opers (U0,u11)) by Def6; A31: u11 is opers_closed by Def7; A32: now__::_thesis:_for_o1_being_operation_of_U1_holds_B_is_closed_on_o1 let o1 be operation of U1; ::_thesis: B is_closed_on o1 consider n being Nat such that A33: n in dom the charact of U1 and A34: o1 = the charact of U1 . n by FINSEQ_2:10; reconsider o0 = the charact of U0 . n as operation of U0 by A29, A30, A33, FUNCT_1:def_3; A35: arity o0 = arity o1 by A33, A34, Th6; A36: u11 is_closed_on o0 by A31, Def4; now__::_thesis:_for_s_being_FinSequence_of_B_st_len_s_=_arity_o1_holds_ o1_._s_in_B let s be FinSequence of B; ::_thesis: ( len s = arity o1 implies o1 . s in B ) A37: P is_closed_on o0 by A6, Def4; reconsider sE = s as Element of P * by A10, A28, FINSEQ_1:def_11; s is FinSequence of u11 by FINSEQ_2:24; then reconsider s1 = s as Element of u11 * by FINSEQ_1:def_11; A38: dom (o0 | ((arity o0) -tuples_on u11)) = (dom o0) /\ ((arity o0) -tuples_on u11) by RELAT_1:61 .= ((arity o0) -tuples_on the carrier of U0) /\ ((arity o0) -tuples_on u11) by MARGREL1:22 .= (arity o0) -tuples_on u11 by MARGREL1:21 ; assume A39: len s = arity o1 ; ::_thesis: o1 . s in B then s1 in { q where q is Element of u11 * : len q = arity o0 } by A35; then A40: s1 in dom (o0 | ((arity o0) -tuples_on u11)) by A38, FINSEQ_2:def_4; o1 . s = (o0 /. u11) . s1 by A29, A33, A34, Def6 .= (o0 | ((arity o0) -tuples_on u11)) . s1 by A36, Def5 .= o0 . sE by A40, FUNCT_1:47 ; hence o1 . s in B by A10, A28, A35, A39, A37, Def3; ::_thesis: verum end; hence B is_closed_on o1 by Def3; ::_thesis: verum end; A41: dom (Opers (U1,B)) = dom the charact of U1 by Def6; A42: dom the charact of U0 = dom (Opers (U0,P)) by Def6; A43: P c= the carrier of U1 by A27, SETFAM_1:3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_the_charact_of_U0_holds_ the_charact_of_E_._n_=_(Opers_(U1,B))_._n let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of E . n = (Opers (U1,B)) . n ) assume A44: n in dom the charact of U0 ; ::_thesis: the charact of E . n = (Opers (U1,B)) . n then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; reconsider o1 = the charact of U1 . n as operation of U1 by A29, A30, A44, FUNCT_1:def_3; A45: u11 is_closed_on o0 by A31, Def4; A46: P is_closed_on o0 by A6, Def4; thus the charact of E . n = o0 /. P by A10, A42, A44, Def6 .= o0 | ((arity o0) -tuples_on P) by A46, Def5 .= o0 | (((arity o0) -tuples_on u11) /\ ((arity o0) -tuples_on P)) by A43, MARGREL1:21 .= (o0 | ((arity o0) -tuples_on u11)) | ((arity o0) -tuples_on P) by RELAT_1:71 .= (o0 /. u11) | ((arity o0) -tuples_on P) by A45, Def5 .= o1 | ((arity o0) -tuples_on P) by A29, A30, A44, Def6 .= o1 | ((arity o1) -tuples_on B) by A10, A28, A29, A30, A44, Th6 .= o1 /. B by A32, Def5 .= (Opers (U1,B)) . n by A29, A30, A41, A44, Def6 ; ::_thesis: verum end; hence ( the charact of E = Opers (U1,B) & B is opers_closed ) by A10, A29, A42, A30, A32, A41, Def4, FINSEQ_1:13; ::_thesis: verum end; uniqueness for b1, b2 being strict SubAlgebra of U0 st A c= the carrier of b1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds b1 is SubAlgebra of U1 ) & A c= the carrier of b2 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds b2 is SubAlgebra of U1 ) holds b1 = b2 proof let W1, W2 be strict SubAlgebra of U0; ::_thesis: ( A c= the carrier of W1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds W1 is SubAlgebra of U1 ) & A c= the carrier of W2 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds W2 is SubAlgebra of U1 ) implies W1 = W2 ) assume ( A c= the carrier of W1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds W1 is SubAlgebra of U1 ) & A c= the carrier of W2 & ( for U2 being SubAlgebra of U0 st A c= the carrier of U2 holds W2 is SubAlgebra of U2 ) ) ; ::_thesis: W1 = W2 then ( W1 is strict SubAlgebra of W2 & W2 is strict SubAlgebra of W1 ) ; hence W1 = W2 by Th10; ::_thesis: verum end; end; :: deftheorem Def12 defines GenUnivAlg UNIALG_2:def_12_:_ for U0 being Universal_Algebra for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds for b3 being strict SubAlgebra of U0 holds ( b3 = GenUnivAlg A iff ( A c= the carrier of b3 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds b3 is SubAlgebra of U1 ) ) ); theorem :: UNIALG_2:18 for U0 being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of U0) = U0 proof let U0 be strict Universal_Algebra; ::_thesis: GenUnivAlg ([#] the carrier of U0) = U0 set W = GenUnivAlg ([#] the carrier of U0); reconsider B = the carrier of (GenUnivAlg ([#] the carrier of U0)) as non empty Subset of U0 by Def7; ( the carrier of (GenUnivAlg ([#] the carrier of U0)) is Subset of U0 & the carrier of U0 c= the carrier of (GenUnivAlg ([#] the carrier of U0)) ) by Def7, Def12; then A1: the carrier of U0 = the carrier of (GenUnivAlg ([#] the carrier of U0)) by XBOOLE_0:def_10; A2: dom the charact of U0 = dom (Opers (U0,B)) by Def6; A3: for n being Nat st n in dom the charact of U0 holds the charact of U0 . n = (Opers (U0,B)) . n proof let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of U0 . n = (Opers (U0,B)) . n ) assume A4: n in dom the charact of U0 ; ::_thesis: the charact of U0 . n = (Opers (U0,B)) . n then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; (Opers (U0,B)) . n = o /. B by A2, A4, Def6; hence the charact of U0 . n = (Opers (U0,B)) . n by A1, Th4; ::_thesis: verum end; the charact of (GenUnivAlg ([#] the carrier of U0)) = Opers (U0,B) by Def7; hence GenUnivAlg ([#] the carrier of U0) = U0 by A1, A2, A3, FINSEQ_1:13; ::_thesis: verum end; theorem Th19: :: UNIALG_2:19 for U0 being Universal_Algebra for U1 being strict SubAlgebra of U0 for B being non empty Subset of U0 st B = the carrier of U1 holds GenUnivAlg B = U1 proof let U0 be Universal_Algebra; ::_thesis: for U1 being strict SubAlgebra of U0 for B being non empty Subset of U0 st B = the carrier of U1 holds GenUnivAlg B = U1 let U1 be strict SubAlgebra of U0; ::_thesis: for B being non empty Subset of U0 st B = the carrier of U1 holds GenUnivAlg B = U1 let B be non empty Subset of U0; ::_thesis: ( B = the carrier of U1 implies GenUnivAlg B = U1 ) set W = GenUnivAlg B; assume A1: B = the carrier of U1 ; ::_thesis: GenUnivAlg B = U1 then GenUnivAlg B is SubAlgebra of U1 by Def12; then A2: the carrier of (GenUnivAlg B) is non empty Subset of U1 by Def7; the carrier of U1 c= the carrier of (GenUnivAlg B) by A1, Def12; then the carrier of U1 = the carrier of (GenUnivAlg B) by A2, XBOOLE_0:def_10; hence GenUnivAlg B = U1 by Th12; ::_thesis: verum end; definition let U0 be Universal_Algebra; let U1, U2 be SubAlgebra of U0; funcU1 "\/" U2 -> strict SubAlgebra of U0 means :Def13: :: UNIALG_2:def 13 for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds it = GenUnivAlg A; existence ex b1 being strict SubAlgebra of U0 st for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds b1 = GenUnivAlg A proof reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ; ( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7; then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8; take GenUnivAlg B ; ::_thesis: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds GenUnivAlg B = GenUnivAlg A thus for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds GenUnivAlg B = GenUnivAlg A ; ::_thesis: verum end; uniqueness for b1, b2 being strict SubAlgebra of U0 st ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds b1 = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds b2 = GenUnivAlg A ) holds b1 = b2 proof reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ; let W1, W2 be strict SubAlgebra of U0; ::_thesis: ( ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds W1 = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds W2 = GenUnivAlg A ) implies W1 = W2 ) assume that A1: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds W1 = GenUnivAlg A and A2: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds W2 = GenUnivAlg A ; ::_thesis: W1 = W2 ( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7; then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8; W1 = GenUnivAlg B by A1; hence W1 = W2 by A2; ::_thesis: verum end; end; :: deftheorem Def13 defines "\/" UNIALG_2:def_13_:_ for U0 being Universal_Algebra for U1, U2 being SubAlgebra of U0 for b4 being strict SubAlgebra of U0 holds ( b4 = U1 "\/" U2 iff for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds b4 = GenUnivAlg A ); theorem Th20: :: UNIALG_2:20 for U0 being Universal_Algebra for U1 being SubAlgebra of U0 for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds (GenUnivAlg A) "\/" U1 = GenUnivAlg B proof let U0 be Universal_Algebra; ::_thesis: for U1 being SubAlgebra of U0 for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds (GenUnivAlg A) "\/" U1 = GenUnivAlg B let U1 be SubAlgebra of U0; ::_thesis: for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds (GenUnivAlg A) "\/" U1 = GenUnivAlg B let A, B be Subset of U0; ::_thesis: ( ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 implies (GenUnivAlg A) "\/" U1 = GenUnivAlg B ) reconsider u1 = the carrier of U1, a = the carrier of (GenUnivAlg A) as non empty Subset of U0 by Def7; assume that A1: ( A <> {} or Constants U0 <> {} ) and A2: B = A \/ the carrier of U1 ; ::_thesis: (GenUnivAlg A) "\/" U1 = GenUnivAlg B A3: A c= the carrier of (GenUnivAlg A) by A1, Def12; A4: B c= the carrier of (GenUnivAlg B) by A2, Def12; A c= B by A2, XBOOLE_1:7; then A5: A c= the carrier of (GenUnivAlg B) by A4, XBOOLE_1:1; now__::_thesis:_(_(_A_<>_{}_&_the_carrier_of_(GenUnivAlg_A)_/\_the_carrier_of_(GenUnivAlg_B)_<>_{}_)_or_(_Constants_U0_<>_{}_&_the_carrier_of_(GenUnivAlg_A)_/\_the_carrier_of_(GenUnivAlg_B)_<>_{}_)_) percases ( A <> {} or Constants U0 <> {} ) by A1; case A <> {} ; ::_thesis: the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} hence the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} by A3, A5, XBOOLE_1:3, XBOOLE_1:19; ::_thesis: verum end; caseA6: Constants U0 <> {} ; ::_thesis: the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} ( Constants U0 is Subset of (GenUnivAlg A) & Constants U0 is Subset of (GenUnivAlg B) ) by Th15; hence the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} by A6, XBOOLE_1:3, XBOOLE_1:19; ::_thesis: verum end; end; end; then the carrier of (GenUnivAlg A) meets the carrier of (GenUnivAlg B) by XBOOLE_0:def_7; then A7: the carrier of ((GenUnivAlg A) /\ (GenUnivAlg B)) = the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by Def9; reconsider b = a \/ u1 as non empty Subset of U0 ; A8: the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) c= a by XBOOLE_1:17; A c= the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by A3, A5, XBOOLE_1:19; then GenUnivAlg A is SubAlgebra of (GenUnivAlg A) /\ (GenUnivAlg B) by A1, A7, Def12; then a is non empty Subset of ((GenUnivAlg A) /\ (GenUnivAlg B)) by Def7; then a = the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by A7, A8, XBOOLE_0:def_10; then A9: a c= the carrier of (GenUnivAlg B) by XBOOLE_1:17; u1 c= B by A2, XBOOLE_1:7; then u1 c= the carrier of (GenUnivAlg B) by A4, XBOOLE_1:1; then b c= the carrier of (GenUnivAlg B) by A9, XBOOLE_1:8; then A10: GenUnivAlg b is strict SubAlgebra of GenUnivAlg B by Def12; A11: (GenUnivAlg A) "\/" U1 = GenUnivAlg b by Def13; then A12: a \/ u1 c= the carrier of ((GenUnivAlg A) "\/" U1) by Def12; A \/ u1 c= a \/ u1 by A3, XBOOLE_1:13; then B c= the carrier of ((GenUnivAlg A) "\/" U1) by A2, A12, XBOOLE_1:1; then GenUnivAlg B is strict SubAlgebra of (GenUnivAlg A) "\/" U1 by A2, Def12; hence (GenUnivAlg A) "\/" U1 = GenUnivAlg B by A11, A10, Th10; ::_thesis: verum end; theorem Th21: :: UNIALG_2:21 for U0 being Universal_Algebra for U1, U2 being SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1 proof let U0 be Universal_Algebra; ::_thesis: for U1, U2 being SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1 let U1, U2 be SubAlgebra of U0; ::_thesis: U1 "\/" U2 = U2 "\/" U1 reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def7; reconsider A = u1 \/ u2 as non empty Subset of U0 ; U1 "\/" U2 = GenUnivAlg A by Def13; hence U1 "\/" U2 = U2 "\/" U1 by Def13; ::_thesis: verum end; theorem Th22: :: UNIALG_2:22 for U0 being with_const_op Universal_Algebra for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1 proof let U0 be with_const_op Universal_Algebra; ::_thesis: for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1 let U1, U2 be strict SubAlgebra of U0; ::_thesis: U1 /\ (U1 "\/" U2) = U1 reconsider u112 = the carrier of (U1 /\ (U1 "\/" U2)) as non empty Subset of U0 by Def7; reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def7; reconsider A = u1 \/ u2 as non empty Subset of U0 ; A1: the charact of U1 = Opers (U0,u1) by Def7; A2: dom (Opers (U0,u1)) = dom the charact of U0 by Def6; U1 "\/" U2 = GenUnivAlg A by Def13; then A3: A c= the carrier of (U1 "\/" U2) by Def12; A4: the carrier of U1 meets the carrier of (U1 "\/" U2) by Th17; then A5: the carrier of (U1 /\ (U1 "\/" U2)) = the carrier of U1 /\ the carrier of (U1 "\/" U2) by Def9; then A6: the carrier of (U1 /\ (U1 "\/" U2)) c= the carrier of U1 by XBOOLE_1:17; the carrier of U1 c= A by XBOOLE_1:7; then the carrier of U1 c= the carrier of (U1 "\/" U2) by A3, XBOOLE_1:1; then A7: the carrier of U1 c= the carrier of (U1 /\ (U1 "\/" U2)) by A5, XBOOLE_1:19; A8: dom (Opers (U0,u112)) = dom the charact of U0 by Def6; A9: for n being Nat st n in dom the charact of U0 holds the charact of (U1 /\ (U1 "\/" U2)) . n = the charact of U1 . n proof let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of (U1 /\ (U1 "\/" U2)) . n = the charact of U1 . n ) assume A10: n in dom the charact of U0 ; ::_thesis: the charact of (U1 /\ (U1 "\/" U2)) . n = the charact of U1 . n then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; thus the charact of (U1 /\ (U1 "\/" U2)) . n = (Opers (U0,u112)) . n by A4, Def9 .= o0 /. u112 by A8, A10, Def6 .= o0 /. u1 by A7, A6, XBOOLE_0:def_10 .= (Opers (U0,u1)) . n by A2, A10, Def6 .= the charact of U1 . n by Def7 ; ::_thesis: verum end; the charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112) by A4, Def9; then the charact of (U1 /\ (U1 "\/" U2)) = the charact of U1 by A1, A8, A2, A9, FINSEQ_1:13; hence U1 /\ (U1 "\/" U2) = U1 by A7, A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th23: :: UNIALG_2:23 for U0 being with_const_op Universal_Algebra for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2 proof let U0 be with_const_op Universal_Algebra; ::_thesis: for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2 let U1, U2 be strict SubAlgebra of U0; ::_thesis: (U1 /\ U2) "\/" U2 = U2 reconsider u12 = the carrier of (U1 /\ U2), u2 = the carrier of U2 as non empty Subset of U0 by Def7; reconsider A = u12 \/ u2 as non empty Subset of U0 ; the carrier of U1 meets the carrier of U2 by Th17; then u12 = the carrier of U1 /\ the carrier of U2 by Def9; then A1: u12 c= u2 by XBOOLE_1:17; (U1 /\ U2) "\/" U2 = GenUnivAlg A by Def13; hence (U1 /\ U2) "\/" U2 = U2 by A1, Th19, XBOOLE_1:12; ::_thesis: verum end; definition let U0 be Universal_Algebra; func Sub U0 -> set means :Def14: :: UNIALG_2:def 14 for x being set holds ( x in it iff x is strict SubAlgebra of U0 ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict SubAlgebra of U0 ) proof reconsider X = { (GenUnivAlg A) where A is Subset of U0 : not A is empty } as set ; take X ; ::_thesis: for x being set holds ( x in X iff x is strict SubAlgebra of U0 ) let x be set ; ::_thesis: ( x in X iff x is strict SubAlgebra of U0 ) thus ( x in X implies x is strict SubAlgebra of U0 ) ::_thesis: ( x is strict SubAlgebra of U0 implies x in X ) proof assume x in X ; ::_thesis: x is strict SubAlgebra of U0 then ex A being Subset of U0 st ( x = GenUnivAlg A & not A is empty ) ; hence x is strict SubAlgebra of U0 ; ::_thesis: verum end; assume x is strict SubAlgebra of U0 ; ::_thesis: x in X then reconsider a = x as strict SubAlgebra of U0 ; reconsider A = the carrier of a as non empty Subset of U0 by Def7; a = GenUnivAlg A by Th19; 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 SubAlgebra of U0 ) ) & ( for x being set holds ( x in b2 iff x is strict SubAlgebra of U0 ) ) holds b1 = b2 proof let A, B be set ; ::_thesis: ( ( for x being set holds ( x in A iff x is strict SubAlgebra of U0 ) ) & ( for x being set holds ( x in B iff x is strict SubAlgebra of U0 ) ) implies A = B ) assume that A1: for x being set holds ( x in A iff x is strict SubAlgebra of U0 ) and A2: for y being set holds ( y in B iff y is strict SubAlgebra of U0 ) ; ::_thesis: A = B now__::_thesis:_for_x_being_set_st_x_in_A_holds_ x_in_B let x be set ; ::_thesis: ( x in A implies x in B ) assume x in A ; ::_thesis: x in B then x is strict SubAlgebra of U0 by A1; hence x in B by A2; ::_thesis: verum end; hence A c= B by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: B c= A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in A ) assume y in B ; ::_thesis: y in A then y is strict SubAlgebra of U0 by A2; hence y in A by A1; ::_thesis: verum end; end; :: deftheorem Def14 defines Sub UNIALG_2:def_14_:_ for U0 being Universal_Algebra for b2 being set holds ( b2 = Sub U0 iff for x being set holds ( x in b2 iff x is strict SubAlgebra of U0 ) ); registration let U0 be Universal_Algebra; cluster Sub U0 -> non empty ; coherence not Sub U0 is empty proof set x = the strict SubAlgebra of U0; the strict SubAlgebra of U0 in Sub U0 by Def14; hence not Sub U0 is empty ; ::_thesis: verum end; end; definition let U0 be Universal_Algebra; func UniAlg_join U0 -> BinOp of (Sub U0) means :Def15: :: UNIALG_2:def 15 for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds it . (x,y) = U1 "\/" U2; existence ex b1 being BinOp of (Sub U0) st for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 "\/" U2 proof defpred S1[ Element of Sub U0, Element of Sub U0, Element of Sub U0] means for U1, U2 being strict SubAlgebra of U0 st \$1 = U1 & \$2 = U2 holds \$3 = U1 "\/" U2; A1: for x, y being Element of Sub U0 ex z being Element of Sub U0 st S1[x,y,z] proof let x, y be Element of Sub U0; ::_thesis: ex z being Element of Sub U0 st S1[x,y,z] reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; reconsider z = U1 "\/" U2 as Element of Sub U0 by Def14; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] ; ::_thesis: verum end; consider o being BinOp of (Sub U0) such that A2: for a, b being Element of Sub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take o ; ::_thesis: for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 "\/" U2 thus for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra 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 (Sub U0) st ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 "\/" U2 ) holds b1 = b2 proof let o1, o2 be BinOp of (Sub U0); ::_thesis: ( ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra 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 Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 "\/" U2 and A4: for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 "\/" U2 ; ::_thesis: o1 = o2 for x, y being Element of Sub U0 holds o1 . (x,y) = o2 . (x,y) proof let x, y be Element of Sub U0; ::_thesis: o1 . (x,y) = o2 . (x,y) reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; 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 Def15 defines UniAlg_join UNIALG_2:def_15_:_ for U0 being Universal_Algebra for b2 being BinOp of (Sub U0) holds ( b2 = UniAlg_join U0 iff for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 "\/" U2 ); definition let U0 be Universal_Algebra; func UniAlg_meet U0 -> BinOp of (Sub U0) means :Def16: :: UNIALG_2:def 16 for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds it . (x,y) = U1 /\ U2; existence ex b1 being BinOp of (Sub U0) st for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 /\ U2 proof defpred S1[ Element of Sub U0, Element of Sub U0, Element of Sub U0] means for U1, U2 being strict SubAlgebra of U0 st \$1 = U1 & \$2 = U2 holds \$3 = U1 /\ U2; A1: for x, y being Element of Sub U0 ex z being Element of Sub U0 st S1[x,y,z] proof let x, y be Element of Sub U0; ::_thesis: ex z being Element of Sub U0 st S1[x,y,z] reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; reconsider z = U1 /\ U2 as Element of Sub U0 by Def14; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] ; ::_thesis: verum end; consider o being BinOp of (Sub U0) such that A2: for a, b being Element of Sub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take o ; ::_thesis: for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 /\ U2 thus for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra 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 (Sub U0) st ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 /\ U2 ) holds b1 = b2 proof let o1, o2 be BinOp of (Sub U0); ::_thesis: ( ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra 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 Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 /\ U2 and A4: for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 /\ U2 ; ::_thesis: o1 = o2 for x, y being Element of Sub U0 holds o1 . (x,y) = o2 . (x,y) proof let x, y be Element of Sub U0; ::_thesis: o1 . (x,y) = o2 . (x,y) reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; 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 Def16 defines UniAlg_meet UNIALG_2:def_16_:_ for U0 being Universal_Algebra for b2 being BinOp of (Sub U0) holds ( b2 = UniAlg_meet U0 iff for x, y being Element of Sub U0 for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 /\ U2 ); theorem Th24: :: UNIALG_2:24 for U0 being Universal_Algebra holds UniAlg_join U0 is commutative proof let U0 be Universal_Algebra; ::_thesis: UniAlg_join U0 is commutative set o = UniAlg_join U0; for x, y being Element of Sub U0 holds (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x) proof let x, y be Element of Sub U0; ::_thesis: (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x) reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ; ( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7; then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8; A1: U1 "\/" U2 = GenUnivAlg B by Def13; ( (UniAlg_join U0) . (x,y) = U1 "\/" U2 & (UniAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def15; hence (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x) by A1, Def13; ::_thesis: verum end; hence UniAlg_join U0 is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th25: :: UNIALG_2:25 for U0 being Universal_Algebra holds UniAlg_join U0 is associative proof let U0 be Universal_Algebra; ::_thesis: UniAlg_join U0 is associative set o = UniAlg_join U0; for x, y, z being Element of Sub U0 holds (UniAlg_join U0) . (x,((UniAlg_join U0) . (y,z))) = (UniAlg_join U0) . (((UniAlg_join U0) . (x,y)),z) proof let x, y, z be Element of Sub U0; ::_thesis: (UniAlg_join U0) . (x,((UniAlg_join U0) . (y,z))) = (UniAlg_join U0) . (((UniAlg_join U0) . (x,y)),z) reconsider U1 = x, U2 = y, U3 = z as strict SubAlgebra of U0 by Def14; reconsider B = the carrier of U1 \/ ( the carrier of U2 \/ the carrier of U3) as non empty set ; A1: (UniAlg_join U0) . (x,y) = U1 "\/" U2 by Def15; A2: the carrier of U2 is Subset of U0 by Def7; A3: the carrier of U3 is Subset of U0 by Def7; then reconsider C = the carrier of U2 \/ the carrier of U3 as non empty Subset of U0 by A2, XBOOLE_1:8; A4: the carrier of U1 is Subset of U0 by Def7; then reconsider D = the carrier of U1 \/ the carrier of U2 as non empty Subset of U0 by A2, XBOOLE_1:8; the carrier of U2 \/ the carrier of U3 c= the carrier of U0 by A2, A3, XBOOLE_1:8; then reconsider B = B as non empty Subset of U0 by A4, XBOOLE_1:8; A5: B = D \/ the carrier of U3 by XBOOLE_1:4; A6: (U1 "\/" U2) "\/" U3 = (GenUnivAlg D) "\/" U3 by Def13 .= GenUnivAlg B by A5, Th20 ; (UniAlg_join U0) . (y,z) = U2 "\/" U3 by Def15; then A7: (UniAlg_join U0) . (x,((UniAlg_join U0) . (y,z))) = U1 "\/" (U2 "\/" U3) by Def15; U1 "\/" (U2 "\/" U3) = U1 "\/" (GenUnivAlg C) by Def13 .= (GenUnivAlg C) "\/" U1 by Th21 .= GenUnivAlg B by Th20 ; hence (UniAlg_join U0) . (x,((UniAlg_join U0) . (y,z))) = (UniAlg_join U0) . (((UniAlg_join U0) . (x,y)),z) by A1, A7, A6, Def15; ::_thesis: verum end; hence UniAlg_join U0 is associative by BINOP_1:def_3; ::_thesis: verum end; theorem Th26: :: UNIALG_2:26 for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is commutative proof let U0 be with_const_op Universal_Algebra; ::_thesis: UniAlg_meet U0 is commutative set o = UniAlg_meet U0; for x, y being Element of Sub U0 holds (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x) proof let x, y be Element of Sub U0; ::_thesis: (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x) reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; A1: ( (UniAlg_meet U0) . (x,y) = U1 /\ U2 & (UniAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def16; A2: the carrier of U1 meets the carrier of U2 by Th17; then ( the carrier of (U2 /\ U1) = the carrier of U2 /\ the carrier of U1 & ( for B2 being non empty Subset of U0 st B2 = the carrier of (U2 /\ U1) holds ( the charact of (U2 /\ U1) = Opers (U0,B2) & B2 is opers_closed ) ) ) by Def9; hence (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x) by A1, A2, Def9; ::_thesis: verum end; hence UniAlg_meet U0 is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th27: :: UNIALG_2:27 for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is associative proof let U0 be with_const_op Universal_Algebra; ::_thesis: UniAlg_meet U0 is associative set o = UniAlg_meet U0; for x, y, z being Element of Sub U0 holds (UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) = (UniAlg_meet U0) . (((UniAlg_meet U0) . (x,y)),z) proof let x, y, z be Element of Sub U0; ::_thesis: (UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) = (UniAlg_meet U0) . (((UniAlg_meet U0) . (x,y)),z) reconsider U1 = x, U2 = y, U3 = z as strict SubAlgebra of U0 by Def14; reconsider u23 = U2 /\ U3, u12 = U1 /\ U2 as Element of Sub U0 by Def14; A1: (UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) = (UniAlg_meet U0) . (x,u23) by Def16 .= U1 /\ (U2 /\ U3) by Def16 ; A2: (UniAlg_meet U0) . (((UniAlg_meet U0) . (x,y)),z) = (UniAlg_meet U0) . (u12,z) by Def16 .= (U1 /\ U2) /\ U3 by Def16 ; the carrier of U2 meets the carrier of U3 by Th17; then A3: the carrier of (U2 /\ U3) = the carrier of U2 /\ the carrier of U3 by Def9; then A4: the carrier of U1 meets the carrier of U2 /\ the carrier of U3 by Th17; then A5: for B being non empty Subset of U0 st B = the carrier of (U1 /\ (U2 /\ U3)) holds ( the charact of (U1 /\ (U2 /\ U3)) = Opers (U0,B) & B is opers_closed ) by A3, Def9; A6: the carrier of (U1 /\ (U2 /\ U3)) = the carrier of U1 /\ ( the carrier of U2 /\ the carrier of U3) by A3, A4, Def9; then reconsider C = the carrier of U1 /\ ( the carrier of U2 /\ the carrier of U3) as non empty Subset of U0 by Def7; A7: C = ( the carrier of U1 /\ the carrier of U2) /\ the carrier of U3 by XBOOLE_1:16; the carrier of U1 meets the carrier of U2 by Th17; then A8: the carrier of (U1 /\ U2) = the carrier of U1 /\ the carrier of U2 by Def9; then the carrier of U1 /\ the carrier of U2 meets the carrier of U3 by Th17; hence (UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) = (UniAlg_meet U0) . (((UniAlg_meet U0) . (x,y)),z) by A1, A2, A8, A6, A5, A7, Def9; ::_thesis: verum end; hence UniAlg_meet U0 is associative by BINOP_1:def_3; ::_thesis: verum end; definition let U0 be with_const_op Universal_Algebra; func UnSubAlLattice U0 -> strict Lattice equals :: UNIALG_2:def 17 LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); coherence LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is strict Lattice proof set L = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); A1: for a, b, c being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider x = a, y = b, z = c as Element of Sub U0 ; A2: UniAlg_join U0 is associative by Th25; thus a "\/" (b "\/" c) = the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,(b "\/" c)) by LATTICES:def_1 .= (UniAlg_join U0) . (x,((UniAlg_join U0) . (y,z))) by LATTICES:def_1 .= the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (( the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,b)),c) by A2, BINOP_1:def_3 .= ( the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,b)) "\/" c by LATTICES:def_1 .= (a "\/" b) "\/" c by LATTICES:def_1 ; ::_thesis: verum end; A3: for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "/\" b = b "/\" a proof let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); ::_thesis: a "/\" b = b "/\" a reconsider x = a, y = b as Element of Sub U0 ; A4: UniAlg_meet U0 is commutative by Th26; thus a "/\" b = (UniAlg_meet U0) . (x,y) by LATTICES:def_2 .= the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (b,a) by A4, BINOP_1:def_2 .= b "/\" a by LATTICES:def_2 ; ::_thesis: verum end; A5: for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "/\" (a "\/" b) = a proof let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); ::_thesis: a "/\" (a "\/" b) = a reconsider x = a, y = b as Element of Sub U0 ; A6: (UniAlg_meet U0) . (x,((UniAlg_join U0) . (x,y))) = x proof reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; (UniAlg_join U0) . (x,y) = U1 "\/" U2 by Def15; hence (UniAlg_meet U0) . (x,((UniAlg_join U0) . (x,y))) = U1 /\ (U1 "\/" U2) by Def16 .= x by Th22 ; ::_thesis: verum end; thus a "/\" (a "\/" b) = the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,(a "\/" b)) by LATTICES:def_2 .= a by A6, LATTICES:def_1 ; ::_thesis: verum end; A7: for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds (a "/\" b) "\/" b = b proof let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); ::_thesis: (a "/\" b) "\/" b = b reconsider x = a, y = b as Element of Sub U0 ; A8: (UniAlg_join U0) . (((UniAlg_meet U0) . (x,y)),y) = y proof reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14; (UniAlg_meet U0) . (x,y) = U1 /\ U2 by Def16; hence (UniAlg_join U0) . (((UniAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def15 .= y by Th23 ; ::_thesis: verum end; thus (a "/\" b) "\/" b = the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . ((a "/\" b),b) by LATTICES:def_1 .= b by A8, LATTICES:def_2 ; ::_thesis: verum end; A9: for a, b, c being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider x = a, y = b, z = c as Element of Sub U0 ; A10: UniAlg_meet U0 is associative by Th27; thus a "/\" (b "/\" c) = the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,(b "/\" c)) by LATTICES:def_2 .= (UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) by LATTICES:def_2 .= the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (( the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,b)),c) by A10, BINOP_1:def_3 .= ( the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a,b)) "/\" c by LATTICES:def_2 .= (a "/\" b) "/\" c by LATTICES:def_2 ; ::_thesis: verum end; for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "\/" b = b "\/" a proof let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); ::_thesis: a "\/" b = b "\/" a reconsider x = a, y = b as Element of Sub U0 ; A11: UniAlg_join U0 is commutative by Th24; thus a "\/" b = (UniAlg_join U0) . (x,y) by LATTICES:def_1 .= the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (b,a) by A11, BINOP_1:def_2 .= b "\/" a by LATTICES:def_1 ; ::_thesis: verum end; then ( LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is join-commutative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is join-associative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is meet-absorbing & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is meet-commutative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is meet-associative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is join-absorbing ) by A1, A7, A3, A9, A5, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is strict Lattice ; ::_thesis: verum end; end; :: deftheorem defines UnSubAlLattice UNIALG_2:def_17_:_ for U0 being with_const_op Universal_Algebra holds UnSubAlLattice U0 = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);