let m be non empty Element of 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 Element of 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 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 Element of 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 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 Element of 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 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 Element of 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 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 Element of 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 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 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

let h be set ; :: 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:21; :: thesis: verum

end;

then A4: [.p,q.] c= dom (f * (reproj i,x)) by TARSKI:def 3;

A5: now

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
set y = (reproj i,x) . x0;
A7: (proj i,m) . ((reproj i,x) . x0) = x0 by Th39, A1;
f is_partial_differentiable_in (reproj i,x) . x0,i by A1, A6;
then f * (reproj i,((reproj i,x) . x0)) is_differentiable_in x0 by A7, PDIFF_1:def 11;
hence f * (reproj i,x) is_differentiable_in x0 by Th40, A1; :: thesis: verum

end;

now

let z be set ; :: 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.] by TARSKI:def 3;
then A9: ].p,q.[ c= dom (f * (reproj i,x)) by A4, XBOOLE_1:1;
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:16;

now

let x0, r be real number ; :: thesis: ( x0 in [.p,q.] & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in [.p,q.] & abs (x1 - x0) < s holds
abs (((f * (reproj i,x)) . x1) - ((f * (reproj i,x)) . x0)) < r ) ) )
assume A11: ( x0 in [.p,q.] & 0 < r ) ; :: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in [.p,q.] & abs (x1 - x0) < s holds
abs (((f * (reproj i,x)) . x1) - ((f * (reproj i,x)) . x0)) < r ) )
then f * (reproj i,x) is_continuous_in x0 by A5, FDIFF_1:32;
then consider s being real number such that
A12: ( 0 < s & ( for x1 being real number st x1 in dom (f * (reproj i,x)) & abs (x1 - x0) < s holds
abs (((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 number st x1 in [.p,q.] & abs (x1 - x0) < s holds
abs (((f * (reproj i,x)) . x1) - ((f * (reproj i,x)) . x0)) < r ) )
thus 0 < s by A12; :: thesis: for x1 being real number st x1 in [.p,q.] & abs (x1 - x0) < s holds
abs (((f * (reproj i,x)) . x1) - ((f * (reproj i,x)) . x0)) < r
thus for x1 being real number st x1 in [.p,q.] & abs (x1 - x0) < s holds
abs (((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:15;
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, ROLLE:3, A4, A10;
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:88;
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 8
.= (f * (reproj i,x)) . p by A4, A15, FUNCT_1:22 ;
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 8
.= (f * (reproj i,x)) . q by A4, A17, FUNCT_1:22 ;
reconsider y = (reproj i,x) . r as Element of REAL m ;
diff (f * (reproj i,x)),r = partdiff f,y,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