let n be non zero Element of NAT ; :: thesis: for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n)
for F being PartFunc of REAL,(REAL-NS n) st a <= b & 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 continuous PartFunc of REAL,(REAL-NS n)
for F being PartFunc of REAL,(REAL-NS n) st a <= b & 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,(REAL-NS n); :: thesis: for F being PartFunc of REAL,(REAL-NS n) st a <= b & 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,(REAL-NS n); :: thesis: ( a <= b & 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 )
assume A1: ( a <= b & 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
reconsider f0 = f, F0 = F as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
A2: f | ['a,b'] is bounded by A1, Th32;
a in [.a,b.] by A1;
then A3: a in ['a,b'] by A1, INTEGRA5:def 3;
A4: f0 is continuous by NFCONT_4:23;

A5: now :: thesis: for t being Real st t in [.a,b.] holds
F0 . t = integral (f0,a,t)

let t be Real; :: thesis: ( t in [.a,b.] implies F0 . t = integral (f0,a,t) )
assume A6: t in [.a,b.] ; :: thesis: F0 . t = integral (f0,a,t)
then A7: t in ['a,b'] by A1, INTEGRA5:def 3;
thus F0 . t = integral (f,a,t) by A1, A6
.= integral (f0,a,t) by A1, A7, A2, Th33, A3, INTEGR19:48 ; :: thesis: verum

end;

now :: thesis: for x being Real st x in [.a,b.] holds
F is_continuous_in x

let x be Real; :: thesis: ( x in [.a,b.] implies F is_continuous_in x )
assume x in [.a,b.] ; :: thesis: F is_continuous_in x
then F0 is_continuous_in x by A4, A5, A1, Th31;
hence F is_continuous_in x by NFCONT_4:1; :: thesis: verum

end;

hence for x being Real st x in [.a,b.] holds
F is_continuous_in x ; :: thesis: verum