let m be non empty Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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;
(reproj i,y) . q = (reproj i,y) . (y . i) by A1, PDIFF_1:def 1;
then (reproj i,y) . q = Replace y,i,(y . i) by PDIFF_1:def 5;
then A3: y = (reproj i,y) . q by FUNCT_7:37;

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 Real st h in [.q,p.] holds
(reproj i,y) . h in X

proof

let h be 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;

A6: now

let h be Real; :: thesis: ( h in [.q,p.] implies (reproj i,y) . h in dom f )
assume h in [.q,p.] ; :: thesis: (reproj i,y) . h in dom f
then (reproj i,y) . h in X by A5;
hence (reproj i,y) . h in dom f by A1; :: thesis: verum

end;

now

let h be Real; :: thesis: ( h in [.q,p.] implies f is_partial_differentiable_in (reproj i,y) . h,i )
assume h in [.q,p.] ; :: thesis: f is_partial_differentiable_in (reproj i,y) . h,i
then (reproj i,y) . h in X by A5;
hence f is_partial_differentiable_in (reproj i,y) . h,i by A1; :: thesis: verum

end;

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

A10: dom y = Seg m by FINSEQ_1:110;
then A11: ( i in dom y & len y = m ) by A1, FINSEQ_1:def 3;
then len (Replace y,i,p) = m by FINSEQ_7:7;
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 8;
then A13: z . i = p by A1, A11, FINSEQ_7:10;
A14: y = (reproj i,z) . q by A1, Th40, A3;
A15: for h being Real st h in [.p,q.] holds
(reproj i,z) . h in X

proof

let h be 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;
hence (reproj i,z) . h in X by A1; :: thesis: verum

end;

A16: for h being Real st h in [.p,q.] holds
(reproj i,z) . h in dom f

proof

let h be Real; :: thesis: ( h in [.p,q.] implies (reproj i,z) . h in dom f )
assume h in [.p,q.] ; :: thesis: (reproj i,z) . h in dom f
then (reproj i,z) . h in X by A15;
hence (reproj i,z) . h in dom f by A1; :: thesis: verum

end;

for h being Real st h in [.p,q.] holds
f is_partial_differentiable_in (reproj i,z) . h,i

proof

let h be Real; :: thesis: ( h in [.p,q.] implies f is_partial_differentiable_in (reproj i,z) . h,i )
assume h in [.p,q.] ; :: thesis: f is_partial_differentiable_in (reproj i,z) . h,i
then (reproj i,z) . h in X by A15;
hence f is_partial_differentiable_in (reproj i,z) . h,i by A1; :: thesis: verum

end;

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;
(reproj i,z) . p = Replace z,i,(z . i) by A13, PDIFF_1:def 5;
then (f /. y) - (f /. z) = (q - p) * (partdiff f,w,i) by FUNCT_7:37, A14, A17;
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;