begin
theorem Th1:
theorem
theorem Th3:
theorem
canceled;
theorem
theorem Th6:
theorem Th7:
:: deftheorem Def1 defines "" EQUATION:def 1 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th14:
theorem Th15:
theorem
theorem
begin
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
begin
:: deftheorem defines TermAlg EQUATION:def 3 :
:: deftheorem defines Equations EQUATION:def 4 :
theorem Th31:
theorem Th32:
:: deftheorem Def5 defines |= EQUATION:def 5 :
:: deftheorem Def6 defines |= EQUATION:def 6 :
theorem Th33:
theorem
theorem Th35:
theorem
theorem Th37:
theorem
Lm1:
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
theorem Th39:
theorem