let n be non zero Element of NAT ; 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; 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); 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); ( 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) ) )
; 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 for t being Real st t in [.a,b.] holds
F0 . t = integral (f0,a,t)let t be
Real;
( t in [.a,b.] implies F0 . t = integral (f0,a,t) )assume A6:
t in [.a,b.]
;
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
;
verum end;
hence
for x being Real st x in [.a,b.] holds
F is_continuous_in x
; verum