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