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) )

per cases ( p = q or p <> q ) ;

suppose A2: p = q ; :: 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) )

then A3: p in [.p,q.] ;
reconsider y = (reproj i,x) . p as Element of REAL m ;
(q - p) * (partdiff f,y,i) = 0 by A2;
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 A3, A2; :: thesis: verum

end;

suppose p <> q ; :: 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) )

then p < q by A1, XXREAL_0:1;
then A4: 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 Th42, A1;
].p,q.[ c= [.p,q.] by XXREAL_1:25;
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 A4; :: thesis: verum

end;

end;