let m be non zero Nat; :: thesis: for f being PartFunc of (REAL m),REAL
for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let f be PartFunc of (REAL m),REAL; :: thesis: for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let X be Subset of (REAL m); :: thesis: for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let x, y, z be Element of REAL m; :: thesis: for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let i be Nat; :: thesis: for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let d, p, q be Real; :: thesis: ( 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y implies ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) ) )
assume A1: ( 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y ) ; :: thesis: ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
then A2: p = (proj (i,m)) . z by Th39;
reconsider yi = y . i as Element of REAL by XREAL_0:def 1;
(reproj (i,y)) . q = (reproj (i,y)) . (y . i) by A1, PDIFF_1:def 1;
then (reproj (i,y)) . q = Replace (y,i,yi) by PDIFF_1:def 5;
then A3: y = (reproj (i,y)) . q by FUNCT_7:35;

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

suppose A4: q <= p ; :: thesis: ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )

A5: for h being Element of REAL st h in [.q,p.] holds
(reproj (i,y)) . h in X

proof

let h be Element of REAL ; :: thesis: ( h in [.q,p.] implies (reproj (i,y)) . h in X )
assume h in [.q,p.] ; :: thesis: (reproj (i,y)) . h in X
then |.(((reproj (i,y)) . h) - x).| < d by A1, Th44;
hence (reproj (i,y)) . h in X by A1; :: thesis: verum

end;

then A6: for h being Real st h in [.q,p.] holds
(reproj (i,y)) . h in dom f by A1;
reconsider p = p, q = q as Real ;
for h being Element of REAL st h in [.q,p.] holds
f is_partial_differentiable_in (reproj (i,y)) . h,i by A1, A5;
then consider r being Real, w being Element of REAL m such that
A7: ( r in [.q,p.] & w = (reproj (i,y)) . r & (f /. ((reproj (i,y)) . p)) - (f /. ((reproj (i,y)) . q)) = (p - q) * (partdiff (f,w,i)) ) by Th43, A1, A4, A6;
A8: |.(w - x).| < d by A7, A1, Th44;
then f is_partial_differentiable_in w,i by A1;
hence ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) ) by A7, A3, A1, A8; :: thesis: verum

end;

suppose A9: p < q ; :: thesis: ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )

reconsider p = p as Element of REAL by XREAL_0:def 1;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A10: dom y = Seg m by FINSEQ_1:89;
then A11: ( i in dom y & len y = mm ) by A1, FINSEQ_1:def 3;
then len (Replace (y,i,p)) = m by FINSEQ_7:5;
then A12: dom y = dom (Replace (y,i,p)) by A10, FINSEQ_1:def 3;
z = Replace (y,i,p) by A1, PDIFF_1:def 5;
then z . i = (Replace (y,i,p)) /. i by A11, A12, PARTFUN1:def 6;
then A13: z . i = p by A1, A11, FINSEQ_7:8;
A14: y = (reproj (i,z)) . q by A1, Th40, A3;
A15: for h being Element of REAL st h in [.p,q.] holds
(reproj (i,z)) . h in X

proof

let h be Element of REAL ; :: thesis: ( h in [.p,q.] implies (reproj (i,z)) . h in X )
assume h in [.p,q.] ; :: thesis: (reproj (i,z)) . h in X
then |.(((reproj (i,z)) . h) - x).| < d by A2, A14, A1, Th44;
then (reproj (i,z)) . h in X by A1;
hence (reproj (i,z)) . h in X ; :: thesis: verum

end;

A16: for h being Real st h in [.p,q.] holds
(reproj (i,z)) . h in dom f by A15, A1;
for h being Element of REAL st h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,z)) . h,i by A15, A1;
then consider r being Real, w being Element of REAL m such that
A17: ( r in [.p,q.] & w = (reproj (i,z)) . r & (f /. ((reproj (i,z)) . q)) - (f /. ((reproj (i,z)) . p)) = (q - p) * (partdiff (f,w,i)) ) by Th43, A1, A9, A16;
A18: |.(w - x).| < d by A2, A14, A17, A1, Th44;
then A19: f is_partial_differentiable_in w,i by A1;
reconsider zi = z . i as Real ;
(reproj (i,z)) . p = Replace (z,i,zi) by A13, PDIFF_1:def 5;
then (f /. y) - (f /. z) = (q - p) * (partdiff (f,w,i)) by A14, A17, FUNCT_7:35;
then (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) ;
hence ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) ) by A18, A19; :: thesis: verum

end;

end;