let m be non zero Element of NAT ; :: thesis: for k being Element of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( f is_continuously_differentiable_up_to_order 1,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 k be Element of NAT ; :: thesis: for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( f is_continuously_differentiable_up_to_order 1,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 non empty Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( f is_continuously_differentiable_up_to_order 1,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 ( f is_continuously_differentiable_up_to_order 1,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.| ) ) ) ) ) )
assume A1: ( X is open & X c= dom f ) ; :: thesis: ( f is_continuously_differentiable_up_to_order 1,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.| ) ) ) ) )

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 f is_continuously_differentiable_up_to_order 1,X )

assume A2: f is_continuously_differentiable_up_to_order 1,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.| ) ) ) )

now :: thesis: for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let i be Nat; :: thesis: ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A3: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
set I = <*ii*>;
A4: len <*ii*> = 1 by FINSEQ_1:40;
i in Seg m by A3;
then {i} c= Seg m by ZFMISC_1:31;
then A5: rng <*ii*> c= Seg m by FINSEQ_1:38;
then A6: f `partial| (X,<*ii*>) is_continuous_on X by A2, A4;
thus f is_partial_differentiable_on X,i by A4, A5, A2, PDIFF_9:def 11, PDIFF_9:81; :: thesis: f `partial| (X,i) is_continuous_on X
hence f `partial| (X,i) is_continuous_on X by A1, A3, PDIFF_9:82, A6; :: thesis: verum

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.| ) ) ) ) by A1, PDIFF_9:63; :: thesis: verum

end;

assume A7: ( 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: f is_continuously_differentiable_up_to_order 1,X
then A8: 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 ) by A1, PDIFF_9:63;

A9: now :: thesis: for I being non empty FinSequence of NAT st len I <= 1 & rng I c= Seg m holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )

let I be non empty FinSequence of NAT ; :: thesis: ( len I <= 1 & rng I c= Seg m implies ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) )
assume A10: ( len I <= 1 & rng I c= Seg m ) ; :: thesis: ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )
A11: 1 <= len I by FINSEQ_1:20;
then 1 in dom I by FINSEQ_3:25;
then A14: I . 1 in rng I by FUNCT_1:3;
reconsider i = I . 1 as Element of NAT by ORDINAL1:def 12;
A15: ( 1 <= i & i <= m ) by A14, A10, FINSEQ_1:1;
A16: I = <*(I . 1)*> by FINSEQ_5:14, A10, A11, XXREAL_0:1;
then A17: I = <*i*> ;
thus f is_partial_differentiable_on X,I by A16, PDIFF_9:81, A15, A8; :: thesis: f `partial| (X,I) is_continuous_on X
f `partial| (X,i) is_continuous_on X by A15, A1, PDIFF_9:63, A7;
hence f `partial| (X,I) is_continuous_on X by A1, A8, A17, A15, PDIFF_9:82; :: thesis: verum

end;

then for I being non empty FinSequence of NAT st len I <= 1 & rng I c= Seg m holds
f is_partial_differentiable_on X,I ;
hence f is_continuously_differentiable_up_to_order 1,X by A1, A9, PDIFF_9:def 11; :: thesis: verum