let m be non zero Nat; for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Nat st 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
let f be PartFunc of (REAL m),REAL; for p, q being Real
for x being Element of REAL m
for i being Nat st 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
let p, q be Real; for x being Element of REAL m
for i being Nat st 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
let x be Element of REAL m; for i being Nat st 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
let i be Nat; ( 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) implies ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) ) )
assume A1:
( 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj (i,x)) . h in dom f ) & ( for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,x)) . h,i ) )
; ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
set g = f * (reproj (i,x));
then A4:
[.p,q.] c= dom (f * (reproj (i,x)))
;
A5:
now for x0 being Real st x0 in [.p,q.] holds
f * (reproj (i,x)) is_differentiable_in x0let x0 be
Real;
( x0 in [.p,q.] implies f * (reproj (i,x)) is_differentiable_in x0 )assume A6:
x0 in [.p,q.]
;
f * (reproj (i,x)) is_differentiable_in x0reconsider xx =
x0 as
Element of
REAL by XREAL_0:def 1;
set y =
(reproj (i,x)) . xx;
A7:
(proj (i,m)) . ((reproj (i,x)) . xx) = x0
by Th39, A1;
f is_partial_differentiable_in (reproj (i,x)) . xx,
i
by A1, A6;
then
f * (reproj (i,((reproj (i,x)) . xx))) is_differentiable_in x0
by A7;
hence
f * (reproj (i,x)) is_differentiable_in x0
by Th40, A1;
verum end;
then A8:
].p,q.[ c= [.p,q.]
;
then A9:
].p,q.[ c= dom (f * (reproj (i,x)))
by A4;
for x being Real st x in ].p,q.[ holds
f * (reproj (i,x)) is_differentiable_in x
by A5, A8;
then A10:
f * (reproj (i,x)) is_differentiable_on ].p,q.[
by A9, FDIFF_1:9;
now for x0, r being Real st x0 in [.p,q.] & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.p,q.] & |.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < r ) )let x0,
r be
Real;
( x0 in [.p,q.] & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.p,q.] & |.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < r ) ) )assume A11:
(
x0 in [.p,q.] &
0 < r )
;
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.p,q.] & |.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < r ) )then
f * (reproj (i,x)) is_continuous_in x0
by A5, FDIFF_1:24;
then consider s being
Real such that A12:
(
0 < s & ( for
x1 being
Real st
x1 in dom (f * (reproj (i,x))) &
|.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < r ) )
by A11, FCONT_1:3;
take s =
s;
( 0 < s & ( for x1 being Real st x1 in [.p,q.] & |.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < r ) )thus
0 < s
by A12;
for x1 being Real st x1 in [.p,q.] & |.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < rthus
for
x1 being
Real st
x1 in [.p,q.] &
|.(x1 - x0).| < s holds
|.(((f * (reproj (i,x))) . x1) - ((f * (reproj (i,x))) . x0)).| < r
by A4, A12;
verum end;
then
(f * (reproj (i,x))) | [.p,q.] is continuous
by A4, FCONT_1:14;
then consider r being Real such that
A13:
( r in ].p,q.[ & diff ((f * (reproj (i,x))),r) = (((f * (reproj (i,x))) . q) - ((f * (reproj (i,x))) . p)) / (q - p) )
by A1, A4, A10, ROLLE:3;
q - p <> 0
by A1;
then A14:
(diff ((f * (reproj (i,x))),r)) * (q - p) = ((f * (reproj (i,x))) . q) - ((f * (reproj (i,x))) . p)
by A13, XCMPLX_1:87;
A15:
p in { s where s is Real : ( p <= s & s <= q ) }
by A1;
then A16: f /. ((reproj (i,x)) . p) =
f . ((reproj (i,x)) . p)
by A1, PARTFUN1:def 6
.=
(f * (reproj (i,x))) . p
by A4, A15, FUNCT_1:12
;
A17:
q in { s where s is Real : ( p <= s & s <= q ) }
by A1;
then A18: f /. ((reproj (i,x)) . q) =
f . ((reproj (i,x)) . q)
by A1, PARTFUN1:def 6
.=
(f * (reproj (i,x))) . q
by A4, A17, FUNCT_1:12
;
reconsider r = r as Element of REAL by XREAL_0:def 1;
set y = (reproj (i,x)) . r;
diff ((f * (reproj (i,x))),r) = partdiff (f,((reproj (i,x)) . r),i)
by A1, Th41;
hence
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj (i,x)) . r & (f /. ((reproj (i,x)) . q)) - (f /. ((reproj (i,x)) . p)) = (q - p) * (partdiff (f,y,i)) )
by A13, A14, A16, A18; verum