let m be non empty Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
let f be PartFunc of (REAL m),REAL; :: thesis: ( X is open & X c= dom f implies ( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) ) )
set g = <>* f;
assume AS1: ( X is open & X c= dom f ) ; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
then AS2: X c= dom (<>* f) by LMXTh0;

hereby :: thesis: ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) implies for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume P1: for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; :: thesis: ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) )
P3: for i being Element of NAT st 1 <= i & i <= m holds
( <>* f is_partial_differentiable_on X,i & (<>* f) `partial| (X,i) is_continuous_on X )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m implies ( <>* f is_partial_differentiable_on X,i & (<>* f) `partial| (X,i) is_continuous_on X ) )
assume P20: ( 1 <= i & i <= m ) ; :: thesis: ( <>* f is_partial_differentiable_on X,i & (<>* f) `partial| (X,i) is_continuous_on X )
then ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by P1;
hence ( <>* f is_partial_differentiable_on X,i & (<>* f) `partial| (X,i) is_continuous_on X ) by AS1, CW020, CW021, P20; :: thesis: verum

end;

then <>* f is_differentiable_on X by CW01, AS1, AS2;
hence f is_differentiable_on X by YTh30; :: thesis: for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )
thus for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) :: thesis: verum

proof

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )
let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) )
assume ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )
then consider s being Real such that
Q2: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| ) ) by P3, CW01, AS1, AS2;
take s ; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )
thus 0 < s by Q2; :: thesis: for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| )
assume Q3: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
let v be Element of REAL m; :: thesis: |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
|.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| by Q3, Q2;
hence |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| by CW022; :: thesis: verum

end;

end;

now :: thesis: ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) implies for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume P1: ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) ; :: thesis: for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then P2: <>* f is_differentiable_on X by AS1, YTh30;
P3: for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| ) )

proof

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| ) )
let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| ) ) )
assume ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| ) )
then consider s being Real such that
Q2: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) by P1;
take s ; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| ) )
thus 0 < s by Q2; :: thesis: for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| )
assume Q3: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
let v be Element of REAL m; :: thesis: |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| by Q3, Q2;
hence |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| by CW022; :: thesis: verum

end;

thus for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume P4: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then P5: ( <>* f is_partial_differentiable_on X,i & (<>* f) `partial| (X,i) is_continuous_on X ) by P3, CW01, AS2, AS1, P2;
hence f is_partial_differentiable_on X,i by P4, CW020, AS1; :: thesis: f `partial| (X,i) is_continuous_on X
hence f `partial| (X,i) is_continuous_on X by P4, P5, CW021, AS1; :: thesis: verum

end;

end;

hence ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) implies for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) ; :: thesis: verum