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

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;

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

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 A7:
( f is_differentiable_on X & ( for x0 being Element of REAL mfor 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.| ) ) ) )

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

hence
( f is_differentiable_on X & ( for x0 being Element of REAL m( 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;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

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

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 )

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 & 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;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

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