let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL

for X being non empty Subset of (REAL m)

for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let f be PartFunc of (REAL m),REAL; :: thesis: for X being non empty Subset of (REAL m)

for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let X be non empty Subset of (REAL m); :: thesis: for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let d be Real; :: thesis: for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let i be Element of NAT ; :: thesis: ( X is open & f = X --> d & 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume A1: X is open ; :: thesis: ( not f = X --> d or not 1 <= i or not i <= m or ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume A2: f = X --> d ; :: thesis: ( not 1 <= i or not i <= m or ( 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 )

A4: dom f = X by A2, FUNCT_2:def 1;

A5: f is_differentiable_on X by Th14, A2, A1;

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 A2, Th13, A1;

hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A3, A4, A1, A5, PDIFF_9:63; :: thesis: verum

for X being non empty Subset of (REAL m)

for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let f be PartFunc of (REAL m),REAL; :: thesis: for X being non empty Subset of (REAL m)

for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let X be non empty Subset of (REAL m); :: thesis: for d being Real

for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let d be Real; :: thesis: for i being Element of NAT st X is open & f = X --> d & 1 <= i & i <= m holds

( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let i be Element of NAT ; :: thesis: ( X is open & f = X --> d & 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume A1: X is open ; :: thesis: ( not f = X --> d or not 1 <= i or not i <= m or ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume A2: f = X --> d ; :: thesis: ( not 1 <= i or not i <= m or ( 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 )

A4: dom f = X by A2, FUNCT_2:def 1;

A5: f is_differentiable_on X by Th14, A2, A1;

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 A2, Th13, A1;

hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A3, A4, A1, A5, PDIFF_9:63; :: thesis: verum