let f be PartFunc of REAL,REAL; :: thesis: ( f is_C^1-Class_on ['0,1'] implies Sum_LWBND_rng_d f = lower_sum ((@' (f,['0,1'])),D[01]) )
assume A1: f is_C^1-Class_on ['0,1'] ; :: thesis: Sum_LWBND_rng_d f = lower_sum ((@' (f,['0,1'])),D[01])
A2: dom (Sum_LWBND_rng_d f) = NAT by FUNCT_2:def 1
.= dom (lower_sum ((@' (f,['0,1'])),D[01])) by FUNCT_2:def 1 ;
for x being object st x in dom (Sum_LWBND_rng_d f) holds
(Sum_LWBND_rng_d f) . x = (lower_sum ((@' (f,['0,1'])),D[01])) . x

proof

let x be object ; :: thesis: ( x in dom (Sum_LWBND_rng_d f) implies (Sum_LWBND_rng_d f) . x = (lower_sum ((@' (f,['0,1'])),D[01])) . x )
assume A4: x in dom (Sum_LWBND_rng_d f) ; :: thesis: (Sum_LWBND_rng_d f) . x = (lower_sum ((@' (f,['0,1'])),D[01])) . x
then reconsider x1 = x as Nat ;
(x1 + 1) * (lower_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(x1 + 1))))) = LWBND_rng_d (f,x1) by A1, Lm17;
then A5: Sum (LWBND_rng_d (f,x1)) = Sum ((x1 + 1) * (lower_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(x1 + 1)))))) by NIVEN:6
.= (x1 + 1) * (Sum (lower_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(x1 + 1)))))) by RVSUM_1:87 ;
(Sum_LWBND_rng_d f) . x1 = (Sum (LWBND_rng_d (f,x1))) / (x1 + 1) by Def11
.= ((1 / (x1 + 1)) * (x1 + 1)) * (Sum (lower_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(x1 + 1)))))) by A5
.= 1 * (Sum (lower_volume ((@' (f,['0,1'])),(EqDiv (['0,1'],(x1 + 1)))))) by XCMPLX_1:106
.= lower_sum ((@' (f,['0,1'])),(D[01] . x1)) by A4, Def1
.= (lower_sum ((@' (f,['0,1'])),D[01])) . x1 by INTEGRA2:def 3 ;
hence (Sum_LWBND_rng_d f) . x = (lower_sum ((@' (f,['0,1'])),D[01])) . x ; :: thesis: verum

end;

hence Sum_LWBND_rng_d f = lower_sum ((@' (f,['0,1'])),D[01]) by A2; :: thesis: verum