begin
begin
begin
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
begin
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
begin
begin
definition
let S be non
empty non
void ManySortedSign ;
let U0 be
non-empty MSAlgebra over
S;
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
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
end;
definition
let S be non
empty non
void ManySortedSign ;
let U0 be
non-empty MSAlgebra over
S;
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
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
end;
:: Subalgebras of a Many Sorted Algebra.
::