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


begin

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

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

begin

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

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

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

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

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

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

registration
cluster non empty non void V60() strict all-with_const_op for ManySortedSign ;
existence
 ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is all-with_const_op & b1 is strict )
proofend;
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 = {} &amp; the ResultSort of S . o = s &amp; 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 &amp; b1 =  {  a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} &amp; the ResultSort of S . o = s &amp; a in rng (Den (o,U0)) )  }  ) ) &amp; ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} ) )
proofend;
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 <> {} &amp; ex A being non empty set st
( A = the Sorts of U0 . s &amp; b1 =  {  a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} &amp; the ResultSort of S . o = s &amp; a in rng (Den (o,U0)) )  }  ) &amp; ex A being non empty set st
( A = the Sorts of U0 . s &amp; b2 =  {  a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} &amp; the ResultSort of S . o = s &amp; a in rng (Den (o,U0)) )  }  ) implies b1 = b2 ) &amp; ( not the Sorts of U0 . s <> {} &amp; b1 = {} &amp; 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 &amp; b4 =  {  a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} &amp; the ResultSort of S . o = s &amp; a in rng (Den (o,U0)) )  }  ) ) ) &amp; ( 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)
proofend;
uniqueness
 for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = Constants (U0,s) ) &amp; ( for s being SortSymbol of S holds b2 . s = Constants (U0,s) ) holds
b1 = b2
proofend;
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
proofend;
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
proofend;
end;

begin

::
:: 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;
predA is_closed_on o means :Def5: :: MSUALG_2:def 5
 rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;
end;

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

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

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

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

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
let A be MSSubset of U0;
assume A1: A is_closed_on o ;
funco /. A ->  Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) equals :Def7: :: MSUALG_2:def 7
(Den (o,U0)) | (((A #) * the Arity of S) . o);
coherence
 (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)
proofend;
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
proofend;
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 ) &amp; ( for o being OperSymbol of S holds b2 . o = o /. A ) holds
b1 = b2
proofend;
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 &amp; ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )
proofend;

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
proofend;

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 &amp; ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed &amp; the Charact of it = Opers (U0,B) ) ) );
existence
 ex b1 being MSAlgebra over S st
( the Sorts of b1 is MSSubset of U0 &amp; ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed &amp; the Charact of b1 = Opers (U0,B) ) ) )
proofend;
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 &amp; ( for B being MSSubset of U0 st B = the Sorts of b3 holds
( B is opers_closed &amp; 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
proofend;

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
proofend;
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 &amp; b1 is strict )
proofend;
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
proofend;

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 &amp; U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2
proofend;

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 &amp; U2 is MSSubAlgebra of U1 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
proofend;

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
proofend;

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

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
proofend;

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()
proofend;

begin

::
:: 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 set holds
( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) &amp; x is MSSubset of U0 &amp; ( for B being MSSubset of U0 st B = x holds
( B is opers_closed &amp; Constants U0 c= B &amp; A c= B ) ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) &amp; x is MSSubset of U0 &amp; ( for B being MSSubset of U0 st B = x holds
( B is opers_closed &amp; Constants U0 c= B &amp; A c= B ) ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) &amp; x is MSSubset of U0 &amp; ( for B being MSSubset of U0 st B = x holds
( B is opers_closed &amp; Constants U0 c= B &amp; A c= B ) ) ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) &amp; x is MSSubset of U0 &amp; ( for B being MSSubset of U0 st B = x holds
( B is opers_closed &amp; Constants U0 c= B &amp; A c= B ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines SubSort MSUALG_2:def_10_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b4 being set holds
( b4 = SubSort A iff for x being set holds
( x in b4 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) &amp; x is MSSubset of U0 &amp; ( for B being MSSubset of U0 st B = x holds
( B is opers_closed &amp; Constants U0 c= B &amp; 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
proofend;

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

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

:: deftheorem Def11 defines SubSort MSUALG_2:def_11_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b3 being set holds
( b3 = SubSort U0 iff for x being set holds
( x in b3 iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) &amp; x is MSSubset of U0 &amp; ( 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
proofend;
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 &amp; Constants U0 c= B &amp; A c= B ) )
proofend;

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 )
proofend;

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

:: deftheorem Def13 defines SubSort MSUALG_2:def_13_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for s being SortSymbol of S
for b5 being set holds
( b5 = SubSort (A,s) iff for x being set holds
( x in b5 iff ex B being MSSubset of U0 st
( B in SubSort A &amp; 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
proofend;
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))
proofend;
uniqueness
 for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s)) ) &amp; ( for s being SortSymbol of S holds b2 . s = meet (SubSort (A,s)) ) holds
b1 = b2
proofend;
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
proofend;

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()
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; A c= MSSubSort A )
proofend;

begin

::
:: 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 ;
funcU0 | A ->  strict MSSubAlgebra of U0 equals :Def15: :: MSUALG_2:def 15
 MSAlgebra(# A,(Opers (U0,A)) #);
coherence
 MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0
proofend;
end;

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

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let U1, U2 be MSSubAlgebra of U0;
funcU1 /\ U2 ->  strict MSSubAlgebra of U0 means :Def16: :: MSUALG_2:def 16
( the Sorts of it = the Sorts of U1 /\ the Sorts of U2 &amp; ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed &amp; 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 &amp; ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed &amp; the Charact of b1 = Opers (U0,B) ) ) )
proofend;
uniqueness
 for b1, b2 being strict MSSubAlgebra of U0 st the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 &amp; ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed &amp; the Charact of b1 = Opers (U0,B) ) ) &amp; the Sorts of b2 = the Sorts of U1 /\ the Sorts of U2 &amp; ( for B being MSSubset of U0 st B = the Sorts of b2 holds
( B is opers_closed &amp; 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 &amp; ( for B being MSSubset of U0 st B = the Sorts of b5 holds
( B is opers_closed &amp; 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 &amp; ( 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 &amp; ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) )
proofend;
uniqueness
 for b1, b2 being strict MSSubAlgebra of U0 st A is MSSubset of b1 &amp; ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) &amp; A is MSSubset of b2 &amp; ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b2 is MSSubAlgebra of U1 ) holds
b1 = b2
proofend;
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 &amp; ( 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
proofend;
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 #)
proofend;

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

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)
proofend;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let U1, U2 be MSSubAlgebra of U0;
funcU1 "\/" U2 ->  strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18
 for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
it = GenMSAlg A;
existence
 ex b1 being strict MSSubAlgebra of U0 st
for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenMSAlg A
proofend;
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 ) &amp; ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b2 = GenMSAlg A ) holds
b1 = b2
proofend;
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
proofend;

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
proofend;

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
proofend;

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

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

begin

::
:: 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 set holds
( x in it iff x is strict MSSubAlgebra of U0 );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 ) ) &amp; ( for x being set holds
( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds
b1 = b2
proofend;
end;

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

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
cluster MSSub U0 ->  non empty ;
coherence
 not MSSub U0 is empty
proofend;
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 &amp; 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 &amp; y = U2 holds
b1 . (x,y) = U1 "\/" U2
proofend;
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 &amp; y = U2 holds
b1 . (x,y) = U1 "\/" U2 ) &amp; ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 &amp; y = U2 holds
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
proofend;
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 &amp; 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 &amp; 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 &amp; y = U2 holds
b1 . (x,y) = U1 /\ U2
proofend;
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 &amp; y = U2 holds
b1 . (x,y) = U1 /\ U2 ) &amp; ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 &amp; y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proofend;
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 &amp; 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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;
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
proofend;

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)
proofend;

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
proofend;

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

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
proofend;