let n be non zero Element of NAT ; :: thesis: for a, b being Real
for f, F being PartFunc of REAL,(REAL n) st a <= b & dom f = ['a,b'] & dom F = ['a,b'] & f is continuous & ( 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, F being PartFunc of REAL,(REAL n) st a <= b & dom f = ['a,b'] & dom F = ['a,b'] & f is continuous & ( 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, F be PartFunc of REAL,(REAL n); :: thesis: ( a <= b & dom f = ['a,b'] & dom F = ['a,b'] & f is continuous & ( 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 )
assume A1: ( a <= b & dom f = ['a,b'] & dom F = ['a,b'] & f is continuous & ( 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
A2: f | ['a,b'] is bounded by A1, Th29;
dom f = dom |.f.| by NFCONT_4:def 2;
then |.f.| | ['a,b'] = |.f.| by A1;
then |.f.| is bounded by A1, A2, INTEGR19:19;
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;
a in [.a,b.] by A1;
then a in ['a,b'] by A1, INTEGRA5:def 3;
then a in dom |.f.| by A1, NFCONT_4:def 2;
then A4: |.(|.f.| . a).| < K by A3;
A5: 0 < K by A4, COMPLEX1:46;

A6: now :: thesis: for c, d being Real st c in ['a,b'] & d in ['a,b'] holds
for y being Real st y in ['(min (c,d)),(max (c,d))'] holds
|.(f /. y).| <= K

let c, d be Real; :: thesis: ( c in ['a,b'] & d in ['a,b'] implies for y being Real st y in ['(min (c,d)),(max (c,d))'] holds
|.(f /. y).| <= K )
assume A7: ( c in ['a,b'] & d in ['a,b'] ) ; :: 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 A8: y in ['(min (c,d)),(max (c,d))'] ; :: thesis: |.(f /. y).| <= K
['(min (c,d)),(max (c,d))'] c= ['a,b'] by A7, A1, INTEGR19:3;
then y in ['a,b'] by A8;
then A9: y in dom |.f.| by NFCONT_4:def 2, A1;
then |.(|.f.| . y).| < K by A3;
then |.(|.f.| /. y).| < K by A9, PARTFUN1:def 6;
then |.|.(f /. y).|.| < K by A9, NFCONT_4:def 2;
hence |.(f /. y).| <= K by ABSVALUE:def 1; :: thesis: verum

end;

A10: now :: thesis: for c, d being Real st c in ['a,b'] & d in ['a,b'] holds
|.(integral (f,c,d)).| <= (n * K) * |.(d - c).|

let c, d be Real; :: thesis: ( c in ['a,b'] & d in ['a,b'] implies |.(integral (f,c,d)).| <= (n * K) * |.(d - c).| )
assume A11: ( c in ['a,b'] & d in ['a,b'] ) ; :: thesis: |.(integral (f,c,d)).| <= (n * K) * |.(d - c).|
then for y being Real st y in ['(min (c,d)),(max (c,d))'] holds
|.(f /. y).| <= K by A6;
hence |.(integral (f,c,d)).| <= (n * K) * |.(d - c).| by A1, A2, Th30, A11, INTEGR19:32; :: thesis: verum

end;

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
then A13: x0 in dom F by INTEGRA5:def 3, A1;
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 A14: 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 ) )
A15: 0 < n * K by A5, XREAL_1:129;
then consider s being Real such that
A16: ( 0 < s & s < r / (n * K) ) by XREAL_1:5, A14, XREAL_1:139;
s * (n * K) < (r / (n * K)) * (n * K) by A15, A16, XREAL_1:68;
then A17: ( 0 < s & (n * K) * s < r ) by A15, XCMPLX_1:87, A16;
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 A19: ( x0 in ['a,b'] & x1 in ['a,b'] ) by A1, A12, INTEGRA5:def 3;
then A20: |.(integral (f,x0,x1)).| <= (n * K) * |.(x1 - x0).| by A10;
(n * K) * |.(x1 - x0).| <= (n * K) * s by A5, A18, XREAL_1:64;
then A21: (n * K) * |.(x1 - x0).| < r by A17, XXREAL_0:2;
A22: ( x0 in [.a,b.] & x1 in [.a,b.] ) by A1, A12, INTEGRA5:def 3, A18;
A23: F /. x0 = F . x0 by A19, A1, PARTFUN1:def 6
.= integral (f,a,x0) by A1, A12 ;
A24: F /. x1 = F . x1 by A18, PARTFUN1:def 6
.= integral (f,a,x1) by A22, A1 ;
reconsider R1 = F /. x0 as Element of n -tuples_on REAL ;
reconsider R2 = integral (f,x0,x1) as Element of n -tuples_on REAL ;
((F /. x0) + (integral (f,x0,x1))) - (F /. x0) = integral (f,x0,x1) by RVSUM_1:42;
then |.((F /. x1) - (F /. x0)).| <= (n * K) * |.(x1 - x0).| by A24, A23, A2, Th30, A19, A1, INTEGR19:31, A20;
hence |.((F /. x1) - (F /. x0)).| < r by A21, XXREAL_0:2; :: thesis: verum

end;

hence F is_continuous_in x0 by A13, NFCONT_4:3; :: thesis: verum