let X be RealNormSpace; for f being PartFunc of REAL, the carrier of X
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let f be PartFunc of REAL, the carrier of X; for A being non empty 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 non empty closed_interval Subset of REAL; for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let a, b be Real; ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) )
consider a1, b1 being Real such that
A1:
a1 <= b1
and
A2:
A = [.a1,b1.]
by MEASURE5:14;
assume
A = [.a,b.]
; integral (f,A) = integral (f,a,b)
then A3:
( a1 = a & b1 = b )
by A2, INTEGRA1:5;
then
integral (f,a,b) = integral (f,['a,b'])
by A1, Def9;
hence
integral (f,A) = integral (f,a,b)
by A1, A2, A3, INTEGRA5:def 3; verum