let f be PartFunc of REAL ,REAL ; :: thesis: for A being closed-interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral f,A = integral f,a,b
let A be closed-interval Subset of REAL ; :: thesis: for a, b being Real st A = [.a,b.] holds
integral f,A = integral f,a,b
let a, b be Real; :: thesis: ( A = [.a,b.] implies integral f,A = integral f,a,b )
assume A1: A = [.a,b.] ; :: thesis: integral f,A = integral f,a,b
consider a1, b1 being Real such that
A2: ( a1 <= b1 & A = [.a1,b1.] ) by INTEGRA1:def 1;
A3: ( a1 = a & b1 = b ) by A1, A2, INTEGRA1:6;
then integral f,a,b = integral f,['a,b'] by A2, Def5;
hence integral f,A = integral f,a,b by A2, A3, Def4; :: thesis: verum