let a, b be real number ; :: thesis: for f being PartFunc of REAL ,REAL
for x0 being real number 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 st
( ].a,b.[ c= dom F & ( for x being real number 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 ; :: thesis: for x0 being real number 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 st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) & F is_differentiable_in x0 & diff F,x0 = f . x0 )
let x0 be real number ; :: 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 st
( ].a,b.[ c= dom F & ( for x being real number 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 such that
A1: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) ) by Lm13;
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 st
( ].a,b.[ c= dom F & ( for x being real number 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, Th28;
hence ex F being PartFunc of REAL ,REAL st
( ].a,b.[ c= dom F & ( for x being real number 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