begin
:: deftheorem Def1 defines complex-valued VALUED_0:def 1 :
:: deftheorem Def2 defines ext-real-valued VALUED_0:def 2 :
:: deftheorem Def3 defines real-valued VALUED_0:def 3 :
:: deftheorem Def4 defines rational-valued VALUED_0:def 4 :
:: deftheorem Def5 defines integer-valued VALUED_0:def 5 :
:: deftheorem Def6 defines natural-valued VALUED_0:def 6 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def7 defines complex-valued VALUED_0:def 7 :
:: deftheorem Def8 defines ext-real-valued VALUED_0:def 8 :
:: deftheorem Def9 defines real-valued VALUED_0:def 9 :
:: deftheorem Def10 defines rational-valued VALUED_0:def 10 :
:: deftheorem Def11 defines integer-valued VALUED_0:def 11 :
:: deftheorem Def12 defines natural-valued VALUED_0:def 12 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def13 defines increasing VALUED_0:def 13 :
:: deftheorem Def14 defines decreasing VALUED_0:def 14 :
:: deftheorem Def15 defines non-decreasing VALUED_0:def 15 :
:: deftheorem Def16 defines non-increasing VALUED_0:def 16 :
:: deftheorem Def17 defines subsequence VALUED_0:def 17 :
theorem
theorem
theorem Th21:
theorem
:: deftheorem defines constant VALUED_0:def 18 :
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem Th28:
theorem
theorem Th30:
theorem
:: deftheorem defines zeroed VALUED_0:def 19 :