begin
begin
:: deftheorem MSUALG_1:def 1 :
canceled;
:: deftheorem MSUALG_1:def 2 :
canceled;
:: deftheorem MSUALG_1:def 3 :
canceled;
:: deftheorem MSUALG_1:def 4 :
canceled;
:: deftheorem MSUALG_1:def 5 :
canceled;
:: deftheorem defines the_arity_of MSUALG_1:def 6 :
:: deftheorem defines the_result_sort_of MSUALG_1:def 7 :
begin
:: deftheorem Def8 defines non-empty MSUALG_1:def 8 :
:: deftheorem defines Args MSUALG_1:def 9 :
:: deftheorem defines Result MSUALG_1:def 10 :
:: deftheorem defines Den MSUALG_1:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
begin
Lm1:
for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of (D * ),D holds dom h = (arity h) -tuples_on D
theorem Th7:
theorem Th8:
theorem Th9:
begin
:: deftheorem Def12 defines segmental MSUALG_1:def 12 :
theorem Th10:
reconsider z = 0 as Element of {0 } by TARSKI:def 1;
Lm2:
for A being Universal_Algebra
for f being Function of (dom (signature A)),({0 } * ) holds
( not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is empty & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
:: deftheorem Def13 defines MSSign MSUALG_1:def 13 :
:: deftheorem defines MSSorts MSUALG_1:def 14 :
:: deftheorem defines MSCharact MSUALG_1:def 15 :
:: deftheorem defines MSAlg MSUALG_1:def 16 :
:: deftheorem Def17 defines the_sort_of MSUALG_1:def 17 :
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
:: deftheorem defines the_charact_of MSUALG_1:def 18 :
:: deftheorem defines 1-Alg MSUALG_1:def 19 :
theorem
theorem