let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for rho being Function of A,REAL
for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) holds
Sum v = vol (B,rho)
let D be Division of A; :: thesis: for rho being Function of A,REAL
for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) holds
Sum v = vol (B,rho)
let rho be Function of A,REAL; :: thesis: for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) holds
Sum v = vol (B,rho)
let B be non empty closed_interval Subset of REAL; :: thesis: for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) holds
Sum v = vol (B,rho)
let v be FinSequence of REAL ; :: thesis: ( B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) implies Sum v = vol (B,rho) )
assume AS: ( B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) ) ; :: thesis: Sum v = vol (B,rho)
dom rho = A by FUNCT_2:def 1;
hence Sum v = vol (B,rho) by AS, LmINTEGR208; :: thesis: verum