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 = ;
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:
per cases ( a > b or a <= b ) ;
suppose a > b ; :: thesis:
end;
suppose X1: a <= b ; :: thesis:
reconsider AB = ['a,b'] as non empty closed_interval Subset of REAL ;
X2: AB = [.a,b.] by ;
then A2: f | AB is bounded by ;
B1: dom f = dom by NORMSP_0:def 2;
then ||.f.|| | AB = by A1, X2;
then ||.f.|| is bounded by ;
then consider K being Real such that
A3: for y being set st y in dom holds
|.( . y).| < K by COMSEQ_2:def 3;
B2: [.a,b.] = AB by ;
then a in AB by X1;
then |.( . 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).|
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 ;
now :: thesis: for y being Real st y in ['(min (c,d)),(max (c,d))'] holds
||.(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 by ;
then |.( . y).| < K by A3;
then |.||.(f /. y).||.| < K by ;
hence ||.(f /. y).|| <= K by ABSVALUE:def 1; :: thesis: verum
end;
hence ||.(integral (f,c,d)).|| <= K * |.(d - c).| by ; :: thesis: verum
end;
for r being Real st 0 < r holds
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
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 ;
s * K < (r / K) * K by ;
then A17: K * s < r by ;
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 ;
then A21: K * |.(x1 - x0).| < r by ;
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 ;
hence ||.((F /. x1) - (F /. x0)).|| < r by ; :: thesis: verum
end;
hence F is_continuous_in x0 by ; :: thesis: verum
end;
end;