begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
:: deftheorem Def1 defines On MEASURE7:def 1 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
REAL in bool REAL
by ZFMISC_1:def 1;
then reconsider G0 = NAT --> REAL as Function of NAT ,(bool REAL ) by FUNCOP_1:57;
Lm1:
rng G0 = {REAL }
by FUNCOP_1:14;
then Lm2:
REAL c= union (rng G0)
by ZFMISC_1:31;
Lm3:
for n being Element of NAT holds G0 . n is Interval
:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :
:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :
:: deftheorem Def4 defines vol MEASURE7:def 4 :
theorem Th13:
:: deftheorem defines vol MEASURE7:def 5 :
:: deftheorem defines vol MEASURE7:def 6 :
:: deftheorem Def7 defines vol MEASURE7:def 7 :
theorem Th14:
:: deftheorem Def8 defines Svc MEASURE7:def 8 :
:: deftheorem defines COMPLEX MEASURE7:def 9 :
:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :
:: deftheorem MEASURE7:def 11 :
canceled;
:: deftheorem MEASURE7:def 12 :
canceled;
:: deftheorem Def13 defines On MEASURE7:def 13 :
reconsider D = NAT --> ({} REAL ) as Function of NAT ,(bool REAL ) ;
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem defines Lmi_sigmaFIELD MEASURE7:def 14 :
:: deftheorem defines L_mi MEASURE7:def 15 :