let n be non zero Element of NAT ; for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let a, b be Real; for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let Z be open Subset of REAL; for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let y0 be VECTOR of (REAL-NS n); for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let f be continuous PartFunc of REAL,(REAL-NS n); for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let g be PartFunc of REAL,(REAL-NS n); ( a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) implies ( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) ) )
assume A1:
( a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) )
; ( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
A2:
f is_integrable_on ['a,b']
by A1, Th33;
A3:
f | ['a,b'] is bounded
by A1, Th32;
A4:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
deffunc H1( Element of REAL ) -> Element of the carrier of (REAL-NS n) = integral (f,a,$1);
consider F0 being Function of REAL,(REAL-NS n) such that
A5:
for x being Element of REAL holds F0 . x = H1(x)
from FUNCT_2:sch 4();
set F = F0 | ['a,b'];
A6: dom (F0 | ['a,b']) =
(dom F0) /\ ['a,b']
by RELAT_1:61
.=
REAL /\ ['a,b']
by FUNCT_2:def 1
.=
['a,b']
by XBOOLE_1:28
;
A7:
now for x being Real st x in [.a,b.] holds
(F0 | ['a,b']) . x = integral (f,a,x)let x be
Real;
( x in [.a,b.] implies (F0 | ['a,b']) . x = integral (f,a,x) )assume
x in [.a,b.]
;
(F0 | ['a,b']) . x = integral (f,a,x)then A8:
x in ['a,b']
by A1, INTEGRA5:def 3;
A9:
x in REAL
by XREAL_0:def 1;
thus (F0 | ['a,b']) . x =
F0 . x
by A8, A6, FUNCT_1:47
.=
integral (
f,
a,
x)
by A5, A9
;
verum end;
A10:
].a,b.[ c= [.a,b.]
by XXREAL_1:25;
A11:
for x being Real st x in [.a,b.] holds
F0 | ['a,b'] is_continuous_in x
by Th34, A1, A6, A7;
A12:
for x being Real st x in ].a,b.[ holds
(F0 | ['a,b']) . x = integral (f,a,x)
by A7, A10;
A13:
Z c= dom (F0 | ['a,b'])
by A1, A6, A10, INTEGRA5:def 3;
A14:
now for x being Real st x in Z holds
( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x )let x be
Real;
( x in Z implies ( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x ) )assume A15:
x in Z
;
( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x )then
f is_continuous_in x
by A10, A4, A1, NFCONT_3:def 2;
hence
(
F0 | ['a,b'] is_differentiable_in x &
diff (
(F0 | ['a,b']),
x)
= f /. x )
by A15, A1, A2, A3, A12, A13, INTEGR19:55;
verum end;
then
for x being Real st x in Z holds
F0 | ['a,b'] is_differentiable_in x
;
then A16:
F0 | ['a,b'] is_differentiable_on Z
by A13, NDIFF_3:10;
set G0 = REAL --> y0;
set G = (REAL --> y0) | ['a,b'];
A17: dom ((REAL --> y0) | ['a,b']) =
(dom (REAL --> y0)) /\ ['a,b']
by RELAT_1:61
.=
REAL /\ ['a,b']
.=
['a,b']
by XBOOLE_1:28
;
A18:
now for x being Real st x in [.a,b.] holds
((REAL --> y0) | ['a,b']) . x = y0let x be
Real;
( x in [.a,b.] implies ((REAL --> y0) | ['a,b']) . x = y0 )assume
x in [.a,b.]
;
((REAL --> y0) | ['a,b']) . x = y0then A19:
x in ['a,b']
by A1, INTEGRA5:def 3;
thus ((REAL --> y0) | ['a,b']) . x =
(REAL --> y0) . x
by A19, A17, FUNCT_1:47
.=
y0
by XREAL_0:def 1, FUNCOP_1:7
;
verum end;
A20:
F0 | ['a,b'] is continuous
by A4, A6, A11, NFCONT_3:def 2;
A21:
((REAL --> y0) | ['a,b']) | Z is V22()
;
then A22:
( (REAL --> y0) | ['a,b'] is_differentiable_on Z & ( for x being Real st x in Z holds
(((REAL --> y0) | ['a,b']) `| Z) . x = 0. (REAL-NS n) ) )
by A17, A1, A10, A4, NDIFF_3:20;
A23:
dom g = (dom (F0 | ['a,b'])) /\ (dom ((REAL --> y0) | ['a,b']))
by A6, A17, A1;
now for x being Element of REAL st x in dom g holds
g /. x = (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x)let x be
Element of
REAL ;
( x in dom g implies g /. x = (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x) )assume A24:
x in dom g
;
g /. x = (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x)A25:
x in [.a,b.]
by A24, A1, INTEGRA5:def 3;
A26:
((REAL --> y0) | ['a,b']) /. x =
((REAL --> y0) | ['a,b']) . x
by A24, A1, A17, PARTFUN1:def 6
.=
y0
by A25, A18
;
A27:
(F0 | ['a,b']) /. x =
(F0 | ['a,b']) . x
by A24, A1, A6, PARTFUN1:def 6
.=
integral (
f,
a,
x)
by A25, A7
;
thus g /. x =
g . x
by A24, PARTFUN1:def 6
.=
(((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x)
by A26, A27, A1, A24
;
verum end;
then A28:
g = ((REAL --> y0) | ['a,b']) + (F0 | ['a,b'])
by A23, VFUNCT_1:def 1;
thus
g is continuous
by A20, A28; ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
A29:
a in ['a,b']
by A1, A4;
A30: 0. (REAL-NS n) =
(integral (f,a,a)) - (integral (f,a,a))
by RLVECT_1:15
.=
((integral (f,a,a)) + (integral (f,a,a))) - (integral (f,a,a))
by A29, A1, Th33, A3, INTEGR19:53
.=
(integral (f,a,a)) + ((integral (f,a,a)) - (integral (f,a,a)))
by RLVECT_1:28
.=
(integral (f,a,a)) + (0. (REAL-NS n))
by RLVECT_1:15
.=
integral (f,a,a)
;
thus g /. a =
g . a
by A1, A29, PARTFUN1:def 6
.=
y0 + (integral (f,a,a))
by A1, A29
.=
y0
by A30
; ( g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
A31:
( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) . x = (diff (((REAL --> y0) | ['a,b']),x)) + (diff ((F0 | ['a,b']),x)) ) )
by A28, A16, A22, A1, A10, A4, NDIFF_3:17;
thus
g is_differentiable_on Z
by A28, A16, A22, A1, A10, A4, NDIFF_3:17; for t being Real st t in Z holds
diff (g,t) = f /. t
thus
for t being Real st t in Z holds
diff (g,t) = f /. t
verumproof
let t be
Real;
( t in Z implies diff (g,t) = f /. t )
assume A32:
t in Z
;
diff (g,t) = f /. t
A33:
diff (
g,
t) =
(g `| Z) . t
by A31, A32, NDIFF_3:def 6
.=
(diff (((REAL --> y0) | ['a,b']),t)) + (diff ((F0 | ['a,b']),t))
by A28, A16, A22, A1, A10, A4, NDIFF_3:17, A32
;
A34:
diff (
((REAL --> y0) | ['a,b']),
t) =
(((REAL --> y0) | ['a,b']) `| Z) . t
by A22, A32, NDIFF_3:def 6
.=
0. (REAL-NS n)
by A21, A17, A1, A10, A4, NDIFF_3:20, A32
;
thus diff (
g,
t) =
(0. (REAL-NS n)) + (f /. t)
by A33, A34, A14, A32
.=
f /. t
;
verum
end;