let a, b, x0 be Real; :: thesis: for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds

ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds

ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 implies ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) )

consider F being PartFunc of REAL,(REAL-NS n) such that

A1: ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) ) by Lm18;

assume ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 ) ; :: thesis: ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

then ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1, Th55;

hence ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1; :: thesis: verum

for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds

ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds

ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 implies ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) )

consider F being PartFunc of REAL,(REAL-NS n) such that

A1: ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) ) by Lm18;

assume ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 ) ; :: thesis: ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

then ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1, Th55;

hence ex F being PartFunc of REAL,(REAL-NS n) st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1; :: thesis: verum