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

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