let X be RealBanachSpace; :: thesis: for a being Real

for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds

integral (f,a,a) = 0. X

let a be Real; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds

integral (f,a,a) = 0. X

let f be continuous PartFunc of REAL, the carrier of X; :: thesis: ( a in dom f implies integral (f,a,a) = 0. X )

assume A1: a in dom f ; :: thesis: integral (f,a,a) = 0. X

[.a,a.] = {a} by XXREAL_1:17;

then A2: [.a,a.] c= dom f by A1, ZFMISC_1:31;

A3: ['a,a'] = [.a,a.] by INTEGRA5:def 3;

then A4: integral (f,['a,a']) = integral (f,a,a) by INTEGR18:16;

vol ['a,a'] = a - a by INTEGRA6:5;

hence integral (f,a,a) = 0. X by A4, A2, A3, INTEGR18:17; :: thesis: verum

for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds

integral (f,a,a) = 0. X

let a be Real; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds

integral (f,a,a) = 0. X

let f be continuous PartFunc of REAL, the carrier of X; :: thesis: ( a in dom f implies integral (f,a,a) = 0. X )

assume A1: a in dom f ; :: thesis: integral (f,a,a) = 0. X

[.a,a.] = {a} by XXREAL_1:17;

then A2: [.a,a.] c= dom f by A1, ZFMISC_1:31;

A3: ['a,a'] = [.a,a.] by INTEGRA5:def 3;

then A4: integral (f,['a,a']) = integral (f,a,a) by INTEGR18:16;

vol ['a,a'] = a - a by INTEGRA6:5;

hence integral (f,a,a) = 0. X by A4, A2, A3, INTEGR18:17; :: thesis: verum