let H be Function of NAT ,[:NAT ,NAT :]; :: thesis: ( H is one-to-one & rng H = [:NAT ,NAT :] implies for k being Element of NAT ex m being Element of NAT st
for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . k <= (Ser (vol G)) . m )
assume that
A1: H is one-to-one and
A2: rng H = [:NAT ,NAT :] ; :: thesis: for k being Element of NAT ex m being Element of NAT st
for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . k <= (Ser (vol G)) . m
reconsider y = D as Element of Funcs NAT ,(bool REAL ) by FUNCT_2:11;
defpred S1[ Element of NAT ] means ex m being Element of NAT st
for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . $1 <= (Ser (vol G)) . m;
A3: S1[ 0 ]
proof
take m = (pr1 H) . 0 ; :: thesis: for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . 0 <= (Ser (vol G)) . m
let F be Function of NAT , bool REAL ; :: thesis: for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . 0 <= (Ser (vol G)) . m
let G be Interval_Covering of F; :: thesis: (Ser ((On G,H) vol )) . 0 <= (Ser (vol G)) . m
reconsider GG = On G,H as Interval_Covering of union (rng F) ;
A4: (Ser (GG vol )) . 0 = (GG vol ) . 0 by SUPINF_2:63;
( (GG vol ) . 0 = diameter (GG . 0 ) & ((G . ((pr1 H) . 0 )) vol ) . ((pr2 H) . 0 ) = diameter ((G . ((pr1 H) . 0 )) . ((pr2 H) . 0 )) ) by Def4;
then (GG vol ) . 0 <= ((G . ((pr1 H) . 0 )) vol ) . ((pr2 H) . 0 ) by A2, Def13;
then (GG vol ) . 0 <= vol (G . ((pr1 H) . 0 )) by Th13, MEASURE6:3;
then A5: (GG vol ) . 0 <= (vol G) . ((pr1 H) . 0 ) by Def7;
for n being Element of NAT holds 0. <= (vol G) . n by Th14;
then vol G is nonnegative by SUPINF_2:58;
then (vol G) . m <= (Ser (vol G)) . m by Th2;
hence (Ser ((On G,H) vol )) . 0 <= (Ser (vol G)) . m by A4, A5, XXREAL_0:2; :: thesis: verum
end;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
given m0 being Element of NAT such that A7: for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . k <= (Ser (vol G)) . m0 ; :: thesis: S1[k + 1]
take m = m0 + ((pr1 H) . (k + 1)); :: thesis: for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . (k + 1) <= (Ser (vol G)) . m
let F be Function of NAT , bool REAL ; :: thesis: for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . (k + 1) <= (Ser (vol G)) . m
let G be Interval_Covering of F; :: thesis: (Ser ((On G,H) vol )) . (k + 1) <= (Ser (vol G)) . m
defpred S2[ Element of NAT , Element of Funcs NAT ,(bool REAL )] means ( ( $1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = (G . $1) . m ) & ( $1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A8: for n being Element of NAT ex y being Element of Funcs NAT ,(bool REAL ) st S2[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs NAT ,(bool REAL ) st S2[n,y]
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose A9: n = (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs NAT ,(bool REAL ) st S2[n,y]
reconsider y = G . n as Element of Funcs NAT ,(bool REAL ) by FUNCT_2:11;
take y ; :: thesis: S2[n,y]
thus S2[n,y] by A9; :: thesis: verum
end;
suppose A10: n <> (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs NAT ,(bool REAL ) st S2[n,y]
take y ; :: thesis: S2[n,y]
thus S2[n,y] by A10, FUNCOP_1:13; :: thesis: verum
end;
end;
end;
consider G0 being Function of NAT , Funcs NAT ,(bool REAL ) such that
A11: for n being Element of NAT holds S2[n,G0 . n] from FUNCT_2:sch 3(A8);
 defpred S3[ Element of NAT , Element of Funcs NAT ,(bool REAL )] means ( ( $1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = (G . $1) . m ) & ( $1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A12: for n being Element of NAT ex y being Element of Funcs NAT ,(bool REAL ) st S3[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs NAT ,(bool REAL ) st S3[n,y]
per cases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
suppose A13: n <> (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs NAT ,(bool REAL ) st S3[n,y]
reconsider y = G . n as Element of Funcs NAT ,(bool REAL ) by FUNCT_2:11;
take y ; :: thesis: S3[n,y]
thus S3[n,y] by A13; :: thesis: verum
end;
suppose A14: n = (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs NAT ,(bool REAL ) st S3[n,y]
take y ; :: thesis: S3[n,y]
thus S3[n,y] by A14, FUNCOP_1:13; :: thesis: verum
end;
end;
end;
consider G1 being Function of NAT , Funcs NAT ,(bool REAL ) such that
A15: for n being Element of NAT holds S3[n,G1 . n] from FUNCT_2:sch 3(A12);
 for n being Element of NAT holds G0 . n is Interval_Covering of D . n
proof
let n be Element of NAT ; :: thesis: G0 . n is Interval_Covering of D . n
consider f0 being Function such that
A16: ( G0 . n = f0 & dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def 2;
reconsider f0 = f0 as Function of NAT , bool REAL by A16, FUNCT_2:4;
D . n = {} by FUNCOP_1:13;
then A17: D . n c= union (rng f0) by XBOOLE_1:2;
for s being Element of NAT holds f0 . s is Interval
proof
let s be Element of NAT ; :: thesis: f0 . s is Interval
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose n = (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
then f0 . s = (G . n) . s by A11, A16;
hence f0 . s is Interval ; :: thesis: verum
end;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
hence f0 . s is Interval by A11, A16; :: thesis: verum
end;
end;
end;
then reconsider f0 = f0 as Interval_Covering of D . n by A17, Def2;
G0 . n = f0 by A16;
hence G0 . n is Interval_Covering of D . n ; :: thesis: verum
end;
then reconsider G0 = G0 as Interval_Covering of D by Def3;
set GG0 = On G0,H;
for n being Element of NAT holds G1 . n is Interval_Covering of D . n
proof
let n be Element of NAT ; :: thesis: G1 . n is Interval_Covering of D . n
consider f0 being Function such that
A18: ( G1 . n = f0 & dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def 2;
reconsider f0 = f0 as Function of NAT , bool REAL by A18, FUNCT_2:4;
D . n = {} by FUNCOP_1:13;
then A19: D . n c= union (rng f0) by XBOOLE_1:2;
for s being Element of NAT holds f0 . s is Interval
proof
let s be Element of NAT ; :: thesis: f0 . s is Interval
per cases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
then f0 . s = (G . n) . s by A15, A18;
hence f0 . s is Interval ; :: thesis: verum
end;
suppose n = (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
hence f0 . s is Interval by A15, A18; :: thesis: verum
end;
end;
end;
then reconsider f0 = f0 as Interval_Covering of D . n by A19, Def2;
G1 . n = f0 by A18;
hence G1 . n is Interval_Covering of D . n ; :: thesis: verum
end;
then reconsider G1 = G1 as Interval_Covering of D by Def3;
set GG1 = On G1,H;
A20: for n being Element of NAT holds (vol G) . n = ((vol G0) . n) + ((vol G1) . n)
proof
let n be Element of NAT ; :: thesis: (vol G) . n = ((vol G0) . n) + ((vol G1) . n)
A21: ( (vol G) . n = vol (G . n) & (vol G0) . n = vol (G0 . n) & (vol G1) . n = vol (G1 . n) ) by Def7;
vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
proof
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose A23: n = (pr1 H) . (k + 1) ; :: thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
SUM ((G . n) vol ) = (SUM ((G0 . n) vol )) + (SUM ((G1 . n) vol ))
proof
for s being Element of NAT holds ((G1 . n) vol ) . s = 0.
proof
let s be Element of NAT ; :: thesis: ((G1 . n) vol ) . s = 0.
diameter ((G1 . n) . s) = 0. by A15, A23, MEASURE5:60;
hence ((G1 . n) vol ) . s = 0. by Def4; :: thesis: verum
end;
then A24: SUM ((G1 . n) vol ) = 0. by Th1;
for s being Element of NAT holds ((G0 . n) vol ) . s <= ((G . n) vol ) . s
proof
let s be Element of NAT ; :: thesis: ((G0 . n) vol ) . s <= ((G . n) vol ) . s
((G0 . n) vol ) . s = diameter ((G0 . n) . s) by Def4
.= diameter ((G . n) . s) by A11, A23
.= ((G . n) vol ) . s by Def4 ;
hence ((G0 . n) vol ) . s <= ((G . n) vol ) . s ; :: thesis: verum
end;
then A25: SUM ((G0 . n) vol ) <= SUM ((G . n) vol ) by SUPINF_2:62;
for s being Element of NAT holds ((G . n) vol ) . s <= ((G0 . n) vol ) . s
proof
let s be Element of NAT ; :: thesis: ((G . n) vol ) . s <= ((G0 . n) vol ) . s
((G0 . n) vol ) . s = diameter ((G0 . n) . s) by Def4
.= diameter ((G . n) . s) by A11, A23
.= ((G . n) vol ) . s by Def4 ;
hence ((G . n) vol ) . s <= ((G0 . n) vol ) . s ; :: thesis: verum
end;
then SUM ((G . n) vol ) <= SUM ((G0 . n) vol ) by SUPINF_2:62;
then SUM ((G . n) vol ) = SUM ((G0 . n) vol ) by A25, XXREAL_0:1;
hence SUM ((G . n) vol ) = (SUM ((G0 . n) vol )) + (SUM ((G1 . n) vol )) by A24, SUPINF_2:18; :: thesis: verum
end;
hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) ; :: thesis: verum
end;
suppose A26: n <> (pr1 H) . (k + 1) ; :: thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
A27: for s being Element of NAT holds ((G1 . n) vol ) . s = ((G . n) vol ) . s
proof
let s be Element of NAT ; :: thesis: ((G1 . n) vol ) . s = ((G . n) vol ) . s
( ((G1 . n) vol ) . s = diameter ((G1 . n) . s) & ((G . n) vol ) . s = diameter ((G . n) . s) ) by Def4;
hence ((G1 . n) vol ) . s = ((G . n) vol ) . s by A15, A26; :: thesis: verum
end;
A28: for s being Element of NAT holds ((G0 . n) vol ) . s = 0.
proof
let s be Element of NAT ; :: thesis: ((G0 . n) vol ) . s = 0.
diameter ((G0 . n) . s) = 0. by A11, A26, MEASURE5:60;
hence ((G0 . n) vol ) . s = 0. by Def4; :: thesis: verum
end;
SUM ((G . n) vol ) = (SUM ((G0 . n) vol )) + (SUM ((G1 . n) vol ))
proof
A30: SUM ((G0 . n) vol ) = 0. by A28, Th1;
for s being Element of NAT holds ((G1 . n) vol ) . s <= ((G . n) vol ) . s by A27;
then A31: SUM ((G1 . n) vol ) <= SUM ((G . n) vol ) by SUPINF_2:62;
for s being Element of NAT holds ((G . n) vol ) . s <= ((G1 . n) vol ) . s by A27;
then SUM ((G . n) vol ) <= SUM ((G1 . n) vol ) by SUPINF_2:62;
then SUM ((G . n) vol ) = SUM ((G1 . n) vol ) by A31, XXREAL_0:1;
hence SUM ((G . n) vol ) = (SUM ((G0 . n) vol )) + (SUM ((G1 . n) vol )) by A30, SUPINF_2:18; :: thesis: verum
end;
hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) ; :: thesis: verum
end;
end;
end;
hence (vol G) . n = ((vol G0) . n) + ((vol G1) . n) by A21; :: thesis: verum
end;
A32: (On G0,H) vol is nonnegative by Th13;
A33: (On G1,H) vol is nonnegative by Th13;
A34: (Ser ((On G0,H) vol )) . (k + 1) <= SUM ((On G0,H) vol ) by Th7, Th13;
A35: (G0 . ((pr1 H) . (k + 1))) vol is nonnegative by Th13;
set N0 = { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ;
A36: { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } c= NAT
proof
let s1 be set ; :: according to TARSKI:def 3 :: thesis: ( not s1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } or s1 in NAT )
assume s1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ; :: thesis: s1 in NAT
then ex s being Element of NAT st
( s = s1 & (pr1 H) . (k + 1) = (pr1 H) . s ) ;
hence s1 in NAT ; :: thesis: verum
end;
k + 1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ;
then reconsider N0 = { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } as non empty Subset of NAT by A36;
defpred S4[ Element of N0, Element of NAT ] means $2 = (pr2 H) . $1;
A37: for s being Element of N0 ex y being Element of NAT st S4[s,y] ;
consider SOS being Function of N0, NAT such that
A38: for s being Element of N0 holds S4[s,SOS . s] from FUNCT_2:sch 3(A37);
 for s1, s2 being set st s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 holds
s1 = s2
proof
let s1, s2 be set ; :: thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 )
assume A39: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 ) ; :: thesis: s1 = s2
then reconsider s1 = s1, s2 = s2 as Element of NAT ;
consider s11 being Element of NAT such that
A40: ( s11 = s1 & (pr1 H) . (k + 1) = (pr1 H) . s11 ) by A39;
consider s22 being Element of NAT such that
A41: ( s22 = s2 & (pr1 H) . (k + 1) = (pr1 H) . s22 ) by A39;
A42: ( SOS . s1 = (pr2 H) . s1 & SOS . s2 = (pr2 H) . s2 ) by A38, A39;
( H . s1 = [((pr1 H) . s1),((pr2 H) . s1)] & H . s2 = [((pr1 H) . s2),((pr2 H) . s2)] ) by Def12;
hence s1 = s2 by A1, A39, A40, A41, A42, FUNCT_2:25; :: thesis: verum
end;
then A43: SOS is one-to-one by FUNCT_2:25;
for s being Element of NAT holds
( ( s in N0 implies ((On G0,H) vol ) . s = (((G0 . ((pr1 H) . (k + 1))) vol ) * SOS) . s ) & ( not s in N0 implies ((On G0,H) vol ) . s = 0. ) )
proof
let s be Element of NAT ; :: thesis: ( ( s in N0 implies ((On G0,H) vol ) . s = (((G0 . ((pr1 H) . (k + 1))) vol ) * SOS) . s ) & ( not s in N0 implies ((On G0,H) vol ) . s = 0. ) )
thus ( s in N0 implies ((On G0,H) vol ) . s = (((G0 . ((pr1 H) . (k + 1))) vol ) * SOS) . s ) :: thesis: ( not s in N0 implies ((On G0,H) vol ) . s = 0. )
proof
assume A44: s in N0 ; :: thesis: ((On G0,H) vol ) . s = (((G0 . ((pr1 H) . (k + 1))) vol ) * SOS) . s
then consider s1 being Element of NAT such that
A45: ( s1 = s & (pr1 H) . (k + 1) = (pr1 H) . s1 ) ;
A46: (pr2 H) . s = SOS . s by A38, A44;
((On G0,H) vol ) . s = diameter ((On G0,H) . s) by Def4
.= diameter ((G0 . ((pr1 H) . (k + 1))) . ((pr2 H) . s)) by A2, A45, Def13
.= ((G0 . ((pr1 H) . (k + 1))) vol ) . (SOS . s) by A46, Def4
.= (((G0 . ((pr1 H) . (k + 1))) vol ) * SOS) . s by A44, FUNCT_2:21 ;
hence ((On G0,H) vol ) . s = (((G0 . ((pr1 H) . (k + 1))) vol ) * SOS) . s ; :: thesis: verum
end;
assume not s in N0 ; :: thesis: ((On G0,H) vol ) . s = 0.
then A47: not (pr1 H) . (k + 1) = (pr1 H) . s ;
((On G0,H) vol ) . s = diameter ((On G0,H) . s) by Def4
.= diameter ((G0 . ((pr1 H) . s)) . ((pr2 H) . s)) by A2, Def13
.= 0. by A11, A47, MEASURE5:60 ;
hence ((On G0,H) vol ) . s = 0. ; :: thesis: verum
end;
then A48: SUM ((On G0,H) vol ) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol ) by A32, A35, A43, Th12;
A49: SUM ((G0 . ((pr1 H) . (k + 1))) vol ) = vol (G0 . ((pr1 H) . (k + 1)))
.= (vol G0) . ((pr1 H) . (k + 1)) by Def7 ;
for s being Element of NAT holds 0. <= (vol G0) . s by Th14;
then A50: vol G0 is nonnegative by SUPINF_2:58;
then A51: (vol G0) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . ((pr1 H) . (k + 1)) by Th2;
(Ser (vol G0)) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . m by A50, SUPINF_2:60;
then A52: SUM ((G0 . ((pr1 H) . (k + 1))) vol ) <= (Ser (vol G0)) . m by A49, A51, XXREAL_0:2;
(Ser ((On G0,H) vol )) . (k + 1) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol ) by A34, A48, XXREAL_0:2;
then A53: (Ser ((On G0,H) vol )) . (k + 1) <= (Ser (vol G0)) . m by A52, XXREAL_0:2;
A54: (Ser ((On G1,H) vol )) . k <= (Ser (vol G1)) . m0 by A7;
(On G1,H) . (k + 1) = (G1 . ((pr1 H) . (k + 1))) . ((pr2 H) . (k + 1)) by A2, Def13
.= {} by A15 ;
then A55: ((On G1,H) vol ) . (k + 1) = 0. by Def4, MEASURE5:60;
(Ser ((On G1,H) vol )) . (k + 1) = ((Ser ((On G1,H) vol )) . k) + (((On G1,H) vol ) . (k + 1)) by SUPINF_2:63;
then A56: (Ser ((On G1,H) vol )) . (k + 1) = (Ser ((On G1,H) vol )) . k by A55, SUPINF_2:18;
for s being Element of NAT holds 0. <= (vol G1) . s by Th14;
then vol G1 is nonnegative by SUPINF_2:58;
then (Ser (vol G1)) . m0 <= (Ser (vol G1)) . m by SUPINF_2:60;
then A57: (Ser ((On G1,H) vol )) . (k + 1) <= (Ser (vol G1)) . m by A54, A56, XXREAL_0:2;
( (On G0,H) vol is nonnegative & (On G1,H) vol is nonnegative ) by Th13;
then A58: ( 0. <= (Ser ((On G0,H) vol )) . (k + 1) & 0. <= (Ser ((On G1,H) vol )) . (k + 1) ) by SUPINF_2:59;
for s being Element of NAT holds 0. <= (vol G0) . s by Th14;
then A59: vol G0 is nonnegative by SUPINF_2:58;
for s being Element of NAT holds 0. <= (vol G1) . s by Th14;
then vol G1 is nonnegative by SUPINF_2:58;
then A60: (Ser (vol G)) . m = ((Ser (vol G0)) . m) + ((Ser (vol G1)) . m) by A20, A59, Th3;
for n being Element of NAT holds ((On G,H) vol ) . n = (((On G0,H) vol ) . n) + (((On G1,H) vol ) . n)
proof
let n be Element of NAT ; :: thesis: ((On G,H) vol ) . n = (((On G0,H) vol ) . n) + (((On G1,H) vol ) . n)
A61: ( ((On G,H) vol ) . n = diameter ((On G,H) . n) & ((On G0,H) vol ) . n = diameter ((On G0,H) . n) & ((On G1,H) vol ) . n = diameter ((On G1,H) . n) ) by Def4;
then A62: ((On G,H) vol ) . n = diameter ((G . ((pr1 H) . n)) . ((pr2 H) . n)) by A2, Def13;
per cases ( (pr1 H) . n = (pr1 H) . (k + 1) or (pr1 H) . n <> (pr1 H) . (k + 1) ) ;
suppose A63: (pr1 H) . n = (pr1 H) . (k + 1) ; :: thesis: ((On G,H) vol ) . n = (((On G0,H) vol ) . n) + (((On G1,H) vol ) . n)
A64: (On G0,H) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def13
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A11, A63 ;
(On G1,H) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def13
.= {} by A15, A63 ;
hence ((On G,H) vol ) . n = (((On G0,H) vol ) . n) + (((On G1,H) vol ) . n) by A61, A62, A64, MEASURE5:60, SUPINF_2:18; :: thesis: verum
end;
suppose A65: (pr1 H) . n <> (pr1 H) . (k + 1) ; :: thesis: ((On G,H) vol ) . n = (((On G0,H) vol ) . n) + (((On G1,H) vol ) . n)
A66: (On G1,H) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def13
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A15, A65 ;
(On G0,H) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def13
.= {} by A11, A65 ;
hence ((On G,H) vol ) . n = (((On G0,H) vol ) . n) + (((On G1,H) vol ) . n) by A61, A62, A66, MEASURE5:60, SUPINF_2:18; :: thesis: verum
end;
end;
end;
then (Ser ((On G,H) vol )) . (k + 1) = ((Ser ((On G0,H) vol )) . (k + 1)) + ((Ser ((On G1,H) vol )) . (k + 1)) by A32, A33, Th3;
hence (Ser ((On G,H) vol )) . (k + 1) <= (Ser (vol G)) . m by A53, A57, A58, A60, MEASURE1:4; :: thesis: verum
end;
thus for k being Element of NAT holds S1[k] from NAT_1:sch 1(A3, A6); :: thesis: verum