let X be RealNormSpace; :: thesis: 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; :: thesis: 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; :: 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) )

consider a1, b1 being Real such that

A1: a1 <= b1 and

A2: A = [.a1,b1.] by MEASURE5:14;

assume A = [.a,b.] ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: 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) )

consider a1, b1 being Real such that

A1: a1 <= b1 and

A2: A = [.a1,b1.] by MEASURE5:14;

assume A = [.a,b.] ; :: thesis: 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; :: thesis: verum