let A be non empty Subset of REAL; :: thesis: for F being Interval_Covering of A
for G being one-to-one FinSequence of bool REAL
for H being FinSequence of ExtREAL st rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) holds
Sum H <= vol F
let F be Interval_Covering of A; :: thesis: for G being one-to-one FinSequence of bool REAL
for H being FinSequence of ExtREAL st rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) holds
Sum H <= vol F
let G be one-to-one FinSequence of bool REAL; :: thesis: for H being FinSequence of ExtREAL st rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) holds
Sum H <= vol F
let H be FinSequence of ExtREAL ; :: thesis: ( rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) implies Sum H <= vol F )
assume that
A1: rng G c= rng F and
A2: dom G = dom H and
A3: for n being Nat holds H . n = diameter (G . n) ; :: thesis: Sum H <= vol F
consider F1 being Interval_Covering of A such that
A4: ( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F ) by A1, Th55;
consider S being sequence of ExtREAL such that
A5: ( Sum H = S . (len H) & S . 0 = 0 & ( for n being Nat st n < len H holds
S . (n + 1) = (S . n) + (H . (n + 1)) ) ) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len H implies S . $1 <= (Ser (F1 vol)) . $1 );
F1 vol is nonnegative by MEASURE7:12;
then A6: S₁[ 0 ] by A5, SUPINF_2:40;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
assume A9: n + 1 <= len H ; :: thesis: S . (n + 1) <= (Ser (F1 vol)) . (n + 1)
then A10: n + 1 in dom G by A2, FINSEQ_3:25, NAT_1:11;
S . (n + 1) = (S . n) + (H . (n + 1)) by A5, A9, NAT_1:13;
then S . (n + 1) = (S . n) + (diameter (G . (n + 1))) by A3;
then S . (n + 1) = (S . n) + (diameter (F1 . (n + 1))) by A4, A10;
then A11: S . (n + 1) = (S . n) + ((F1 vol) . (n + 1)) by MEASURE7:def 4;
(S . n) + ((F1 vol) . (n + 1)) <= ((Ser (F1 vol)) . n) + ((F1 vol) . (n + 1)) by A8, A9, NAT_1:13, XXREAL_3:35;
hence S . (n + 1) <= (Ser (F1 vol)) . (n + 1) by A11, SUPINF_2:def 11; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
then A12: Sum H <= (Ser (F1 vol)) . (len H) by A5;
(Ser (F1 vol)) . (len H) <= SUM (F1 vol) by MEASURE7:6, MEASURE7:12;
then Sum H <= SUM (F1 vol) by A12, XXREAL_0:2;
hence Sum H <= vol F by A4, MEASURE7:def 6; :: thesis: verum