let X be RealBanachSpace; :: thesis: for a, b being Real
for y0 being VECTOR of X
for f being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) holds
g /. a = y0
let a, b be Real; :: thesis: for y0 being VECTOR of X
for f being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) holds
g /. a = y0
let y0 be VECTOR of X; :: thesis: for f being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) holds
g /. a = y0
let f be continuous PartFunc of REAL, the carrier of X; :: thesis: for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) holds
g /. a = y0
let g be PartFunc of REAL, the carrier of X; :: thesis: ( a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) implies g /. a = y0 )
assume that
A1: a <= b and
A2: dom f = [.a,b.] and
A6: for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ; :: thesis: g /. a = y0
A4: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then a in ['a,b'] by A1;
then ( integral (f,a,a) = 0. X & g /. a = y0 + (integral (f,a,a)) ) by A2, A6, A4, Lm00;
hence g /. a = y0 ; :: thesis: verum