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