begin
:: deftheorem defines R_EAL MESFUN7C:def 1 :
theorem Th1:
:: deftheorem defines inf MESFUN7C:def 2 :
theorem Th2:
:: deftheorem defines sup MESFUN7C:def 3 :
theorem Th3:
:: deftheorem defines inferior_realsequence MESFUN7C:def 4 :
theorem Th4:
:: deftheorem defines superior_realsequence MESFUN7C:def 5 :
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
theorem
theorem Th11:
:: deftheorem defines lim_inf MESFUN7C:def 6 :
theorem Th12:
:: deftheorem defines lim_sup MESFUN7C:def 7 :
theorem Th13:
:: deftheorem defines lim MESFUN7C:def 8 :
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
begin
:: deftheorem Def9 defines # MESFUN7C:def 9 :
:: deftheorem Def10 defines lim MESFUN7C:def 10 :
:: deftheorem Def11 defines Re MESFUN7C:def 11 :
:: deftheorem Def12 defines Im MESFUN7C:def 12 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem
begin
theorem
Lm1:
for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
begin
:: deftheorem Def13 defines is_simple_func_in MESFUN7C:def 13 :
:: deftheorem Def14 defines are_Re-presentation_of MESFUN7C:def 14 :
:: deftheorem Def15 defines are_Re-presentation_of MESFUN7C:def 15 :
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem