let m be non zero Element of NAT ; :: thesis: for I being non empty FinSequence of NAT

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & 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: for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg 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 f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg 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 d being Real st X is open & f = X --> d & rng I c= Seg m holds

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

let d be Real; :: thesis: ( X is open & f = X --> d & rng I c= Seg m implies ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) )

assume A1: ( X is open & f = X --> d & rng I c= Seg m ) ; :: thesis: ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )

for i being Element of NAT st i <= (len I) - 1 holds

(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)

reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;

A6: f `partial| (X,I) = ((PartDiffSeq (f,X,I)) . k) `partial| (X,(I /. (k + 1))) by PDIFF_9:def 7;

A7: (len I) - 1 <= (len I) - 0 by XREAL_1:10;

for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & 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: for X being non empty Subset of (REAL m)

for f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg 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 f being PartFunc of (REAL m),REAL

for d being Real st X is open & f = X --> d & rng I c= Seg 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 d being Real st X is open & f = X --> d & rng I c= Seg m holds

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

let d be Real; :: thesis: ( X is open & f = X --> d & rng I c= Seg m implies ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) )

assume A1: ( X is open & f = X --> d & rng I c= Seg m ) ; :: thesis: ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )

for i being Element of NAT st i <= (len I) - 1 holds

(PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)

proof

hence
f is_partial_differentiable_on X,I
; :: thesis: f `partial| (X,I) is_continuous_on X
let i be Element of NAT ; :: thesis: ( i <= (len I) - 1 implies (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1) )

assume A2: i <= (len I) - 1 ; :: thesis: (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)

(len I) - 1 <= (len I) - 0 by XREAL_1:10;

then A3: i <= len I by A2, XXREAL_0:2;

end;assume A2: i <= (len I) - 1 ; :: thesis: (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)

(len I) - 1 <= (len I) - 0 by XREAL_1:10;

then A3: i <= len I by A2, XXREAL_0:2;

per cases
( i = 0 or i <> 0 )
;

end;

suppose
i = 0
; :: thesis: (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)

then A4:
(PartDiffSeq (f,X,I)) . i = X --> d
by A1, Th17;

( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) by Lm1, A1, A2;

hence (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1) by A4, A1, Th15; :: thesis: verum

end;( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) by Lm1, A1, A2;

hence (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1) by A4, A1, Th15; :: thesis: verum

suppose
i <> 0
; :: thesis: (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1)

then
1 <= i
by NAT_1:14;

then A5: (PartDiffSeq (f,X,I)) . i = X --> 0 by A1, A3, Th17;

( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) by Lm1, A1, A2;

hence (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1) by A5, A1, Th15; :: thesis: verum

end;then A5: (PartDiffSeq (f,X,I)) . i = X --> 0 by A1, A3, Th17;

( 1 <= I /. (i + 1) & I /. (i + 1) <= m ) by Lm1, A1, A2;

hence (PartDiffSeq (f,X,I)) . i is_partial_differentiable_on X,I /. (i + 1) by A5, A1, Th15; :: thesis: verum

reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;

A6: f `partial| (X,I) = ((PartDiffSeq (f,X,I)) . k) `partial| (X,(I /. (k + 1))) by PDIFF_9:def 7;

A7: (len I) - 1 <= (len I) - 0 by XREAL_1:10;