begin
:: deftheorem defines DOMS VALUED_2:def 1 :
:: deftheorem Def2 defines complex-functions-membered VALUED_2:def 2 :
:: deftheorem Def3 defines ext-real-functions-membered VALUED_2:def 3 :
:: deftheorem Def4 defines real-functions-membered VALUED_2:def 4 :
:: deftheorem Def5 defines rational-functions-membered VALUED_2:def 5 :
:: deftheorem Def6 defines integer-functions-membered VALUED_2:def 6 :
:: deftheorem Def7 defines natural-functions-membered VALUED_2:def 7 :
consider ff being natural-valued Function;
:: deftheorem Def8 defines C_PFuncs VALUED_2:def 8 :
:: deftheorem Def9 defines C_Funcs VALUED_2:def 9 :
:: deftheorem Def10 defines E_PFuncs VALUED_2:def 10 :
:: deftheorem Def11 defines E_Funcs VALUED_2:def 11 :
:: deftheorem Def12 defines R_PFuncs VALUED_2:def 12 :
:: deftheorem Def13 defines R_Funcs VALUED_2:def 13 :
:: deftheorem Def14 defines Q_PFuncs VALUED_2:def 14 :
:: deftheorem Def15 defines Q_Funcs VALUED_2:def 15 :
:: deftheorem Def16 defines I_PFuncs VALUED_2:def 16 :
:: deftheorem Def17 defines I_Funcs VALUED_2:def 17 :
:: deftheorem Def18 defines N_PFuncs VALUED_2:def 18 :
:: deftheorem Def19 defines N_Funcs VALUED_2:def 19 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def20 defines complex-functions-valued VALUED_2:def 20 :
:: deftheorem Def21 defines ext-real-functions-valued VALUED_2:def 21 :
:: deftheorem Def22 defines real-functions-valued VALUED_2:def 22 :
:: deftheorem Def23 defines rational-functions-valued VALUED_2:def 23 :
:: deftheorem Def24 defines integer-functions-valued VALUED_2:def 24 :
:: deftheorem Def25 defines natural-functions-valued VALUED_2:def 25 :
:: deftheorem defines complex-functions-valued VALUED_2:def 26 :
:: deftheorem defines ext-real-functions-valued VALUED_2:def 27 :
:: deftheorem defines real-functions-valued VALUED_2:def 28 :
:: deftheorem defines rational-functions-valued VALUED_2:def 29 :
:: deftheorem defines integer-functions-valued VALUED_2:def 30 :
:: deftheorem defines natural-functions-valued VALUED_2:def 31 :
begin
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
:: deftheorem defines (/) VALUED_2:def 32 :
theorem
theorem
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def33 defines <-> VALUED_2:def 33 :
theorem
theorem
:: deftheorem defines (-) VALUED_2:def 34 :
:: deftheorem Def35 defines </> VALUED_2:def 35 :
theorem
:: deftheorem Def36 defines abs VALUED_2:def 36 :
theorem
:: deftheorem Def37 defines [+] VALUED_2:def 37 :
theorem
theorem
:: deftheorem defines [-] VALUED_2:def 38 :
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def39 defines [#] VALUED_2:def 39 :
theorem
theorem
:: deftheorem defines [/] VALUED_2:def 40 :
theorem
theorem
theorem
theorem
:: deftheorem Def41 defines <+> VALUED_2:def 41 :
theorem
theorem
:: deftheorem defines <-> VALUED_2:def 42 :
theorem Th61:
theorem Th62:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def43 defines <#> VALUED_2:def 43 :
theorem
theorem
theorem
:: deftheorem defines </> VALUED_2:def 44 :
theorem Th71:
theorem Th72:
theorem
:: deftheorem Def45 defines <++> VALUED_2:def 45 :
theorem
theorem
theorem
:: deftheorem Def46 defines <--> VALUED_2:def 46 :
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def47 defines <##> VALUED_2:def 47 :
theorem Th83:
theorem
theorem
theorem
theorem Th87:
theorem
theorem Th89:
theorem
:: deftheorem Def48 defines <//> VALUED_2:def 48 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem