:: Subalgebras of a Many Sorted Algebra. Lattice of Subalgebras
:: by Ewa Burakowska
::
:: Received April 25, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users


registration
let I be set ;
let X be ManySortedSet of I;
let Y be V8() ManySortedSet of I;
cluster X (\/) Y -> V8() ;
coherence
X (\/) Y is non-empty
proof end;
cluster Y (\/) X -> V8() ;
coherence
Y (\/) X is non-empty ;
end;

theorem Th1: :: MSUALG_2:1
for I being non empty set
for X, Y being ManySortedSet of I
for i being Element of I * holds product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))
proof end;

definition
let S be non empty ManySortedSign ;
let U0 be MSAlgebra over S;
mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;
end;

definition
let S be non empty ManySortedSign ;
let IT be SortSymbol of S;
attr IT is with_const_op means :: MSUALG_2:def 1
 ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT );
end;

:: deftheorem defines with_const_op MSUALG_2:def 1 :
for S being non empty ManySortedSign
for IT being SortSymbol of S holds
( IT is with_const_op iff ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT ) );

definition
let IT be non empty ManySortedSign ;
attr IT is all-with_const_op means :Def2: :: MSUALG_2:def 2
 for s being SortSymbol of IT holds s is with_const_op ;
end;

:: deftheorem Def2 defines all-with_const_op MSUALG_2:def 2 :
for IT being non empty ManySortedSign holds
( IT is all-with_const_op iff for s being SortSymbol of IT holds s is with_const_op );

registration
let A be non empty set ;
let B be set ;
let a be Function of B,(A *);
let r be Function of B,A;
cluster ManySortedSign(# A,B,a,r #) -> non empty ;
coherence
not ManySortedSign(# A,B,a,r #) is empty ;
end;

registration
cluster non empty non void V63() strict all-with_const_op for ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is all-with_const_op & b1 is strict )
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let s be SortSymbol of S;
func Constants (U0,s) -> Subset of ( the Sorts of U0 . s) means :Def3: :: MSUALG_2:def 3
 ex A being non empty set st
( A = the Sorts of U0 . s & it = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) if the Sorts of U0 . s <> {}
otherwise it = {} ;
existence
( ( the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) ex A being non empty set st
( A = the Sorts of U0 . s & b1 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) & ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} ) )
proof end;
correctness
consistency
for b1 being Subset of ( the Sorts of U0 . s) holds verum;
uniqueness
for b1, b2 being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} & ex A being non empty set st
( A = the Sorts of U0 . s & b1 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) & ex A being non empty set st
( A = the Sorts of U0 . s & b2 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) implies b1 = b2 ) & ( not the Sorts of U0 . s <> {} & b1 = {} & b2 = {} implies b1 = b2 ) );
;
end;

:: deftheorem Def3 defines Constants MSUALG_2:def 3 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for s being SortSymbol of S
for b4 being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} implies ( b4 = Constants (U0,s) iff ex A being non empty set st
( A = the Sorts of U0 . s & b4 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) ) & ( not the Sorts of U0 . s <> {} implies ( b4 = Constants (U0,s) iff b4 = {} ) ) );

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
func Constants U0 -> MSSubset of U0 means :Def4: :: MSUALG_2:def 4
 for s being SortSymbol of S holds it . s = Constants (U0,s);
existence
ex b1 being MSSubset of U0 st
for s being SortSymbol of S holds b1 . s = Constants (U0,s)
proof end;
uniqueness
for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds b2 . s = Constants (U0,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Constants MSUALG_2:def 4 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b3 being MSSubset of U0 holds
( b3 = Constants U0 iff for s being SortSymbol of S holds b3 . s = Constants (U0,s) );

registration
let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let s be SortSymbol of S;
cluster Constants (U0,s) -> non empty ;
coherence
not Constants (U0,s) is empty
proof end;
end;

registration
let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
cluster Constants U0 -> V8() ;
coherence
Constants U0 is non-empty
proof end;
end;

::
:: Subalgebras of a Many Sorted Algebra.
::
definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
let A be MSSubset of U0;
pred A is_closed_on o means :: MSUALG_2:def 5
 rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;
end;

:: deftheorem defines is_closed_on MSUALG_2:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S
for A being MSSubset of U0 holds
( A is_closed_on o iff rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o );

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
attr A is opers_closed means :: MSUALG_2:def 6
 for o being OperSymbol of S holds A is_closed_on o;
end;

:: deftheorem defines opers_closed MSUALG_2:def 6 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( A is opers_closed iff for o being OperSymbol of S holds A is_closed_on o );

theorem Th2: :: MSUALG_2:2
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for B0, B1 being MSSubset of U0 st B0 c= B1 holds
((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
let A be MSSubset of U0;
assume A1: A is_closed_on o ;
func o /. A -> Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) equals :Def7: :: MSUALG_2:def 7
(Den (o,U0)) | (((A #) * the Arity of S) . o);
coherence
(Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)
proof end;
end;

:: deftheorem Def7 defines /. MSUALG_2:def 7 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S
for A being MSSubset of U0 st A is_closed_on o holds
o /. A = (Den (o,U0)) | (((A #) * the Arity of S) . o);

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
func Opers (U0,A) -> ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S means :Def8: :: MSUALG_2:def 8
 for o being OperSymbol of S holds it . o = o /. A;
existence
ex b1 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = o /. A
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = o /. A ) & ( for o being OperSymbol of S holds b2 . o = o /. A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Opers MSUALG_2:def 8 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b4 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds
( b4 = Opers (U0,A) iff for o being OperSymbol of S holds b4 . o = o /. A );

theorem Th3: :: MSUALG_2:3
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )
proof end;

theorem Th4: :: MSUALG_2:4
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Opers (U0,B) = the Charact of U0
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
mode MSSubAlgebra of U0 -> MSAlgebra over S means :Def9: :: MSUALG_2:def 9
( the Sorts of it is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );
existence
ex b1 being MSAlgebra over S st
( the Sorts of b1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) )
proof end;
end;

:: deftheorem Def9 defines MSSubAlgebra MSUALG_2:def 9 :
for S being non empty non void ManySortedSign
for U0, b3 being MSAlgebra over S holds
( b3 is MSSubAlgebra of U0 iff ( the Sorts of b3 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b3 holds
( B is opers_closed & the Charact of b3 = Opers (U0,B) ) ) ) );

Lm1: for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0
proof end;

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
cluster strict for MSSubAlgebra of U0;
existence
ex b1 being MSSubAlgebra of U0 st b1 is strict
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
cluster MSAlgebra(# the Sorts of U0, the Charact of U0 #) -> non-empty ;
coherence
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is non-empty by MSUALG_1:def 3;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
cluster strict non-empty for MSSubAlgebra of U0;
existence
ex b1 being MSSubAlgebra of U0 st
( b1 is non-empty & b1 is strict )
proof end;
end;

theorem :: MSUALG_2:5
for S being non empty non void ManySortedSign
for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds
U0 is MSSubAlgebra of U1
proof end;

theorem :: MSUALG_2:6
for S being non empty non void ManySortedSign
for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2
proof end;

theorem Th7: :: MSUALG_2:7
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
proof end;

theorem Th8: :: MSUALG_2:8
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds
U1 is MSSubAlgebra of U2
proof end;

theorem Th9: :: MSUALG_2:9
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
proof end;

theorem Th10: :: MSUALG_2:10
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
proof end;

theorem :: MSUALG_2:11
for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V8() MSSubset of U1 by Th10;

theorem :: MSUALG_2:12
for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()
proof end;

::
:: Many Sorted Subsets of a Many Sorted Algebra.
::
definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
func SubSort A -> set means :Def10: :: MSUALG_2:def 10
 for x being object holds
( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being object holds
( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines SubSort MSUALG_2:def 10 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b4 being set holds
( b4 = SubSort A iff for x being object holds
( x in b4 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) );

Lm2: for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A
proof end;

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
cluster SubSort A -> non empty ;
coherence
not SubSort A is empty by Lm2;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
func SubSort U0 -> set means :Def11: :: MSUALG_2:def 11
 for x being object holds
( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) ) & ( for x being object holds
( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b3 being set holds
( b3 = SubSort U0 iff for x being object holds
( x in b3 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
cluster SubSort U0 -> non empty ;
coherence
not SubSort U0 is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let e be Element of SubSort U0;
func @ e -> MSSubset of U0 equals :: MSUALG_2:def 12
e;
coherence
e is MSSubset of U0 by Def11;
end;

:: deftheorem defines @ MSUALG_2:def 12 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for e being Element of SubSort U0 holds @ e = e;

theorem Th13: :: MSUALG_2:13
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
proof end;

theorem Th14: :: MSUALG_2:14
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
let s be SortSymbol of S;
func SubSort (A,s) -> set means :Def13: :: MSUALG_2:def 13
 for x being object holds
( x in it iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) & ( for x being object holds
( x in b2 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines SubSort MSUALG_2:def 13 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for s being SortSymbol of S
for b5 being set holds
( b5 = SubSort (A,s) iff for x being object holds
( x in b5 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
let s be SortSymbol of S;
cluster SubSort (A,s) -> non empty ;
coherence
not SubSort (A,s) is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
func MSSubSort A -> MSSubset of U0 means :Def14: :: MSUALG_2:def 14
 for s being SortSymbol of S holds it . s = meet (SubSort (A,s));
existence
ex b1 being MSSubset of U0 st
for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s))
proof end;
uniqueness
for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds b2 . s = meet (SubSort (A,s)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines MSSubSort MSUALG_2:def 14 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A, b4 being MSSubset of U0 holds
( b4 = MSSubSort A iff for s being SortSymbol of S holds b4 . s = meet (SubSort (A,s)) );

theorem Th15: :: MSUALG_2:15
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds (Constants U0) (\/) A c= MSSubSort A
proof end;

theorem Th16: :: MSUALG_2:16
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 st (Constants U0) (\/) A is V8() holds
MSSubSort A is V8()
proof end;

theorem Th17: :: MSUALG_2:17
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 st B in SubSort A holds
(((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o
proof end;

theorem Th18: :: MSUALG_2:18
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 st B in SubSort A holds
rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
proof end;

theorem Th19: :: MSUALG_2:19
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
proof end;

theorem Th20: :: MSUALG_2:20
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )
proof end;

::
:: Operations on Subalgebras of a Many Sorted Algebra.
::
definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
assume A1: A is opers_closed ;
func U0 | A -> strict MSSubAlgebra of U0 equals :Def15: :: MSUALG_2:def 15
 MSAlgebra(# A,(Opers (U0,A)) #);
coherence
MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0
proof end;
end;

:: deftheorem Def15 defines | MSUALG_2:def 15 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 st A is opers_closed holds
U0 | A = MSAlgebra(# A,(Opers (U0,A)) #);

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let U1, U2 be MSSubAlgebra of U0;
func U1 /\ U2 -> strict MSSubAlgebra of U0 means :Def16: :: MSUALG_2:def 16
( the Sorts of it = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );
existence
ex b1 being strict MSSubAlgebra of U0 st
( the Sorts of b1 = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) )
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st the Sorts of b1 = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) & the Sorts of b2 = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b2 holds
( B is opers_closed & the Charact of b2 = Opers (U0,B) ) ) holds
b1 = b2 by Th9;
end;

:: deftheorem Def16 defines /\ MSUALG_2:def 16 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0
for b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 /\ U2 iff ( the Sorts of b5 = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b5 holds
( B is opers_closed & the Charact of b5 = Opers (U0,B) ) ) ) );

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
func GenMSAlg A -> strict MSSubAlgebra of U0 means :Def17: :: MSUALG_2:def 17
( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
it is MSSubAlgebra of U1 ) );
existence
ex b1 being strict MSSubAlgebra of U0 st
( A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) )
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) & A is MSSubset of b2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b2 is MSSubAlgebra of U1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines GenMSAlg MSUALG_2:def 17 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b4 being strict MSSubAlgebra of U0 holds
( b4 = GenMSAlg A iff ( A is MSSubset of b4 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b4 is MSSubAlgebra of U1 ) ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let A be V8() MSSubset of U0;
cluster GenMSAlg A -> strict non-empty ;
coherence
GenMSAlg A is non-empty
proof end;
end;

theorem Th21: :: MSUALG_2:21
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)
proof end;

theorem Th22: :: MSUALG_2:22
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
proof end;

theorem Th23: :: MSUALG_2:23
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let U1, U2 be MSSubAlgebra of U0;
func U1 "\/" U2 -> strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18
 for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
it = GenMSAlg A;
existence
ex b1 being strict MSSubAlgebra of U0 st
for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b1 = GenMSAlg A
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b2 = GenMSAlg A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines "\/" MSUALG_2:def 18 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0
for b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b5 = GenMSAlg A );

theorem Th24: :: MSUALG_2:24
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0
for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenMSAlg A) "\/" U1 = GenMSAlg B
proof end;

theorem Th25: :: MSUALG_2:25
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
proof end;

theorem Th26: :: MSUALG_2:26
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
proof end;

theorem Th27: :: MSUALG_2:27
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
proof end;

theorem Th28: :: MSUALG_2:28
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
proof end;

::
:: The Lattice of SubAlgebras of a Many Sorted Algebra.
::
definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
func MSSub U0 -> set means :Def19: :: MSUALG_2:def 19
 for x being object holds
( x in it iff x is strict MSSubAlgebra of U0 );
existence
ex b1 being set st
for x being object holds
( x in b1 iff x is strict MSSubAlgebra of U0 )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff x is strict MSSubAlgebra of U0 ) ) & ( for x being object holds
( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines MSSub MSUALG_2:def 19 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b3 being set holds
( b3 = MSSub U0 iff for x being object holds
( x in b3 iff x is strict MSSubAlgebra of U0 ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
cluster MSSub U0 -> non empty ;
coherence
not MSSub U0 is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
func MSAlg_join U0 -> BinOp of (MSSub U0) means :Def20: :: MSUALG_2:def 20
 for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 "\/" U2;
existence
ex b1 being BinOp of (MSSub U0) st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/" U2
proof end;
uniqueness
for b1, b2 being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines MSAlg_join MSUALG_2:def 20 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for b3 being BinOp of (MSSub U0) holds
( b3 = MSAlg_join U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b3 . (x,y) = U1 "\/" U2 );

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
func MSAlg_meet U0 -> BinOp of (MSSub U0) means :Def21: :: MSUALG_2:def 21
 for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 /\ U2;
existence
ex b1 being BinOp of (MSSub U0) st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2
proof end;
uniqueness
for b1, b2 being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines MSAlg_meet MSUALG_2:def 21 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for b3 being BinOp of (MSSub U0) holds
( b3 = MSAlg_meet U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b3 . (x,y) = U1 /\ U2 );

theorem Th29: :: MSUALG_2:29
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative
proof end;

theorem Th30: :: MSUALG_2:30
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative
proof end;

theorem Th31: :: MSUALG_2:31
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative
proof end;

theorem Th32: :: MSUALG_2:32
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
func MSSubAlLattice U0 -> strict Lattice equals :: MSUALG_2:def 22
 LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);
coherence
LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice
proof end;
end;

:: deftheorem defines MSSubAlLattice MSUALG_2:def 22 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

theorem Th33: :: MSUALG_2:33
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded
proof end;

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
cluster MSSubAlLattice U0 -> strict bounded ;
coherence
MSSubAlLattice U0 is bounded by Th33;
end;

theorem :: MSUALG_2:34
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)
proof end;

theorem Th35: :: MSUALG_2:35
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Top (MSSubAlLattice U0) = GenMSAlg B
proof end;

theorem :: MSUALG_2:36
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)
proof end;

theorem :: MSUALG_2:37
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;

theorem :: MSUALG_2:38
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A by Lm2;

theorem :: MSUALG_2:39
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds SubSort A c= SubSort U0
proof end;