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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

let d be Real; :: thesis: ( X is open & f = X --> d & rng I c= Seg m implies ( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) ) )

assume A1: ( X is open & f = X --> d & rng I c= Seg m ) ; :: thesis: ( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

thus A2: (PartDiffSeq (f,X,I)) . 0 = (X --> d) | X by A1, PDIFF_9:def 7

.= (X /\ X) --> d by FUNCOP_1:12

.= X --> d ; :: thesis: for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len I implies (PartDiffSeq (f,X,I)) . $1 = X --> 0 );

A3: S_{1}[ 0 ]
;

A4: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A3, A4);

hence for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ; :: thesis: verum

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

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

( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

let d be Real; :: thesis: ( X is open & f = X --> d & rng I c= Seg m implies ( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) ) )

assume A1: ( X is open & f = X --> d & rng I c= Seg m ) ; :: thesis: ( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ) )

thus A2: (PartDiffSeq (f,X,I)) . 0 = (X --> d) | X by A1, PDIFF_9:def 7

.= (X /\ X) --> d by FUNCOP_1:12

.= X --> d ; :: thesis: for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0

defpred S

A3: S

A4: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A5: S_{1}[i]
; :: thesis: S_{1}[i + 1]

assume A6: ( 1 <= i + 1 & i + 1 <= len I ) ; :: thesis: (PartDiffSeq (f,X,I)) . (i + 1) = X --> 0

A7: i <= i + 1 by NAT_1:12;

end;assume A5: S

assume A6: ( 1 <= i + 1 & i + 1 <= len I ) ; :: thesis: (PartDiffSeq (f,X,I)) . (i + 1) = X --> 0

A7: i <= i + 1 by NAT_1:12;

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

end;

suppose A8:
i = 0
; :: thesis: (PartDiffSeq (f,X,I)) . (i + 1) = X --> 0

A9:
( 1 <= I /. (i + 1) & I /. (i + 1) <= m )
by Lm2, A1, A6;

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

.= X --> 0 by A8, A9, A1, A2, Th16 ; :: thesis: verum

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

.= X --> 0 by A8, A9, A1, A2, Th16 ; :: thesis: verum

suppose A10:
i <> 0
; :: thesis: (PartDiffSeq (f,X,I)) . (i + 1) = X --> 0

A11:
( 1 <= I /. (i + 1) & I /. (i + 1) <= m )
by Lm2, A1, A6;

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

.= X --> 0 by A10, A11, A1, Th16, A7, A5, NAT_1:14, XXREAL_0:2, A6 ; :: thesis: verum

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

.= X --> 0 by A10, A11, A1, Th16, A7, A5, NAT_1:14, XXREAL_0:2, A6 ; :: thesis: verum

hence for i being Element of NAT st 1 <= i & i <= len I holds

(PartDiffSeq (f,X,I)) . i = X --> 0 ; :: thesis: verum