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

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