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)) )
per cases
( p = q or p <> q )
;
suppose A2:
p = q
;
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 p =
p as
Element of
REAL by XREAL_0:def 1;
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;
verum end; suppose
p <> q
;
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;
verum end; end;