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

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

let a, b be Real; :: thesis: for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

let F be PartFunc of REAL, the carrier of X; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

let f be continuous PartFunc of REAL, the carrier of X; :: thesis: ( dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) implies for x being Real st x in [.a,b.] holds

F is_continuous_in x )

set f1 = ||.f.||;

assume A1: ( dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) ) ; :: thesis: for x being Real st x in [.a,b.] holds

F is_continuous_in x

let x0 be Real; :: thesis: ( x0 in [.a,b.] implies F is_continuous_in x0 )

assume A12: x0 in [.a,b.] ; :: thesis: F is_continuous_in x0

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

let a, b be Real; :: thesis: for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

let F be PartFunc of REAL, the carrier of X; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) holds

for x being Real st x in [.a,b.] holds

F is_continuous_in x

let f be continuous PartFunc of REAL, the carrier of X; :: thesis: ( dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) implies for x being Real st x in [.a,b.] holds

F is_continuous_in x )

set f1 = ||.f.||;

assume A1: ( dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds

F /. t = integral (f,a,t) ) ) ; :: thesis: for x being Real st x in [.a,b.] holds

F is_continuous_in x

let x0 be Real; :: thesis: ( x0 in [.a,b.] implies F is_continuous_in x0 )

assume A12: x0 in [.a,b.] ; :: thesis: F is_continuous_in x0

per cases
( a > b or a <= b )
;

end;

suppose X1:
a <= b
; :: thesis: F is_continuous_in x0

reconsider AB = ['a,b'] as non empty closed_interval Subset of REAL ;

X2: AB = [.a,b.] by X1, INTEGRA5:def 3;

then A2: f | AB is bounded by A1, X1, INTEGR21:11;

B1: dom f = dom ||.f.|| by NORMSP_0:def 2;

then ||.f.|| | AB = ||.f.|| by A1, X2;

then ||.f.|| is bounded by A1, A2, X2, INTEGR21:9;

then consider K being Real such that

A3: for y being set st y in dom ||.f.|| holds

|.(||.f.|| . y).| < K by COMSEQ_2:def 3;

B2: [.a,b.] = AB by X1, INTEGRA5:def 3;

then a in AB by X1;

then |.(||.f.|| . a).| < K by A1, X2, B1, A3;

then A5: 0 < K by COMPLEX1:46;

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) )

end;X2: AB = [.a,b.] by X1, INTEGRA5:def 3;

then A2: f | AB is bounded by A1, X1, INTEGR21:11;

B1: dom f = dom ||.f.|| by NORMSP_0:def 2;

then ||.f.|| | AB = ||.f.|| by A1, X2;

then ||.f.|| is bounded by A1, A2, X2, INTEGR21:9;

then consider K being Real such that

A3: for y being set st y in dom ||.f.|| holds

|.(||.f.|| . y).| < K by COMSEQ_2:def 3;

B2: [.a,b.] = AB by X1, INTEGRA5:def 3;

then a in AB by X1;

then |.(||.f.|| . a).| < K by A1, X2, B1, A3;

then A5: 0 < K by COMPLEX1:46;

A6: now :: thesis: for c, d being Real st c in ['a,b'] & d in ['a,b'] holds

||.(integral (f,c,d)).|| <= K * |.(d - c).|

for r being Real st 0 < r holds ||.(integral (f,c,d)).|| <= K * |.(d - c).|

let c, d be Real; :: thesis: ( c in ['a,b'] & d in ['a,b'] implies ||.(integral (f,c,d)).|| <= K * |.(d - c).| )

assume A11: ( c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ||.(integral (f,c,d)).|| <= K * |.(d - c).|

then A7: ['(min (c,d)),(max (c,d))'] c= ['a,b'] by X1, INTEGR19:3;

end;assume A11: ( c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ||.(integral (f,c,d)).|| <= K * |.(d - c).|

then A7: ['(min (c,d)),(max (c,d))'] c= ['a,b'] by X1, INTEGR19:3;

now :: thesis: for y being Real st y in ['(min (c,d)),(max (c,d))'] holds

||.(f /. y).|| <= K

hence
||.(integral (f,c,d)).|| <= K * |.(d - c).|
by A1, X1, X2, A11, INTEGR21:25; :: thesis: verum||.(f /. y).|| <= K

let y be Real; :: thesis: ( y in ['(min (c,d)),(max (c,d))'] implies ||.(f /. y).|| <= K )

assume y in ['(min (c,d)),(max (c,d))'] ; :: thesis: ||.(f /. y).|| <= K

then y in ['a,b'] by A7;

then A9: y in dom ||.f.|| by X2, NORMSP_0:def 2, A1;

then |.(||.f.|| . y).| < K by A3;

then |.||.(f /. y).||.| < K by A9, NORMSP_0:def 2;

hence ||.(f /. y).|| <= K by ABSVALUE:def 1; :: thesis: verum

end;assume y in ['(min (c,d)),(max (c,d))'] ; :: thesis: ||.(f /. y).|| <= K

then y in ['a,b'] by A7;

then A9: y in dom ||.f.|| by X2, NORMSP_0:def 2, A1;

then |.(||.f.|| . y).| < K by A3;

then |.||.(f /. y).||.| < K by A9, NORMSP_0:def 2;

hence ||.(f /. y).|| <= K by ABSVALUE:def 1; :: thesis: verum

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) )

proof

hence
F is_continuous_in x0
by A1, A12, NFCONT_3:8; :: thesis: verum
let r be Real; :: thesis: ( 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) ) )

assume 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) )

then consider s being Real such that

A16: ( 0 < s & s < r / K ) by A5, XREAL_1:5, XREAL_1:139;

s * K < (r / K) * K by A5, A16, XREAL_1:68;

then A17: K * s < r by A5, XCMPLX_1:87;

take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) )

thus 0 < s by A16; :: thesis: for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r

let x1 be Real; :: thesis: ( x1 in dom F & |.(x1 - x0).| < s implies ||.((F /. x1) - (F /. x0)).|| < r )

assume A18: ( x1 in dom F & |.(x1 - x0).| < s ) ; :: thesis: ||.((F /. x1) - (F /. x0)).|| < r

then A20: ||.(integral (f,x0,x1)).|| <= K * |.(x1 - x0).| by A1, A12, B2, A6;

K * |.(x1 - x0).| <= K * s by A5, A18, XREAL_1:64;

then A21: K * |.(x1 - x0).| < r by A17, XXREAL_0:2;

A23: ( F /. x0 = integral (f,a,x0) & F /. x1 = integral (f,a,x1) ) by A1, A12, A18;

reconsider R1 = F /. x0 as VECTOR of X ;

reconsider R2 = integral (f,x0,x1) as VECTOR of X ;

((F /. x0) + (integral (f,x0,x1))) - (F /. x0) = ((F /. x0) + (- (F /. x0))) + (integral (f,x0,x1)) by RLVECT_1:def 3

.= (0. X) + (integral (f,x0,x1)) by RLVECT_1:5

.= integral (f,x0,x1) ;

then ||.((F /. x1) - (F /. x0)).|| <= K * |.(x1 - x0).| by A23, A1, X1, A12, B2, A18, INTEGR21:29, A20;

hence ||.((F /. x1) - (F /. x0)).|| < r by A21, XXREAL_0:2; :: thesis: verum

end;( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) ) )

assume 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) )

then consider s being Real such that

A16: ( 0 < s & s < r / K ) by A5, XREAL_1:5, XREAL_1:139;

s * K < (r / K) * K by A5, A16, XREAL_1:68;

then A17: K * s < r by A5, XCMPLX_1:87;

take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r ) )

thus 0 < s by A16; :: thesis: for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds

||.((F /. x1) - (F /. x0)).|| < r

let x1 be Real; :: thesis: ( x1 in dom F & |.(x1 - x0).| < s implies ||.((F /. x1) - (F /. x0)).|| < r )

assume A18: ( x1 in dom F & |.(x1 - x0).| < s ) ; :: thesis: ||.((F /. x1) - (F /. x0)).|| < r

then A20: ||.(integral (f,x0,x1)).|| <= K * |.(x1 - x0).| by A1, A12, B2, A6;

K * |.(x1 - x0).| <= K * s by A5, A18, XREAL_1:64;

then A21: K * |.(x1 - x0).| < r by A17, XXREAL_0:2;

A23: ( F /. x0 = integral (f,a,x0) & F /. x1 = integral (f,a,x1) ) by A1, A12, A18;

reconsider R1 = F /. x0 as VECTOR of X ;

reconsider R2 = integral (f,x0,x1) as VECTOR of X ;

((F /. x0) + (integral (f,x0,x1))) - (F /. x0) = ((F /. x0) + (- (F /. x0))) + (integral (f,x0,x1)) by RLVECT_1:def 3

.= (0. X) + (integral (f,x0,x1)) by RLVECT_1:5

.= integral (f,x0,x1) ;

then ||.((F /. x1) - (F /. x0)).|| <= K * |.(x1 - x0).| by A23, A1, X1, A12, B2, A18, INTEGR21:29, A20;

hence ||.((F /. x1) - (F /. x0)).|| < r by A21, XXREAL_0:2; :: thesis: verum