begin
:: deftheorem Def1 defines homogeneous UNIALG_1:def 1 :
:: deftheorem defines quasi_total UNIALG_1:def 2 :
theorem
canceled;
theorem Th2:
theorem Th3:
:: deftheorem UNIALG_1:def 3 :
canceled;
:: deftheorem Def4 defines homogeneous UNIALG_1:def 4 :
:: deftheorem Def5 defines quasi_total UNIALG_1:def 5 :
:: deftheorem UNIALG_1:def 6 :
canceled;
:: deftheorem Def7 defines partial UNIALG_1:def 7 :
:: deftheorem Def8 defines quasi_total UNIALG_1:def 8 :
:: deftheorem Def9 defines non-empty UNIALG_1:def 9 :
theorem Th4:
:: deftheorem defines arity UNIALG_1:def 10 :
theorem Th5:
:: deftheorem defines signature UNIALG_1:def 11 :
begin