:: 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) #);