let m be non zero Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) ; :: thesis: 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));
now :: thesis: for h being object st h in [.p,q.] holds
h in dom (f * (reproj (i,x)))
let h be object ; :: thesis: ( h in [.p,q.] implies h in dom (f * (reproj (i,x))) )
assume A2: h in [.p,q.] ; :: thesis: h in dom (f * (reproj (i,x)))
then reconsider h1 = h as Element of REAL ;
A3: dom (reproj (i,x)) = REAL by PDIFF_1:def 5;
(reproj (i,x)) . h1 in dom f by A1, A2;
hence h in dom (f * (reproj (i,x))) by A3, FUNCT_1:11; :: thesis: verum
end;
then A4: [.p,q.] c= dom (f * (reproj (i,x))) ;
A5: now :: thesis: for x0 being Real st x0 in [.p,q.] holds
f * (reproj (i,x)) is_differentiable_in x0
let x0 be Real; :: thesis: ( x0 in [.p,q.] implies f * (reproj (i,x)) is_differentiable_in x0 )
assume A6: x0 in [.p,q.] ; :: thesis: f * (reproj (i,x)) is_differentiable_in x0
reconsider 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; :: thesis: verum
end;
now :: thesis: for z being object st z in ].p,q.[ holds
z in [.p,q.]
let z be object ; :: thesis: ( z in ].p,q.[ implies z in [.p,q.] )
assume z in ].p,q.[ ; :: thesis: z in [.p,q.]
then ex z1 being Real st
( z = z1 & p < z1 & z1 < q ) ;
hence z in [.p,q.] ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( 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; :: thesis: 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 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; :: thesis: 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; :: thesis: verum