let f be PartFunc of (REAL 2),REAL; :: thesis: for z0 being Element of REAL 2

for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

let z0 be Element of REAL 2; :: thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

let N be Neighbourhood of (proj (1,2)) . z0; :: thesis: ( f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) implies for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) ) )

assume that

A1: f is_partial_differentiable_in z0,1 and

A2: N c= dom (SVF1 (1,f,z0)) ; :: thesis: for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

consider x0, y0 being Real such that

A3: z0 = <*x0,y0*> and

A4: ex N1 being Neighbourhood of x0 st

( N1 c= dom (SVF1 (1,f,z0)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Th9;

consider N1 being Neighbourhood of x0 such that

N1 c= dom (SVF1 (1,f,z0)) and

A5: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;

A6: (proj (1,2)) . z0 = x0 by A3, Th1;

then consider N2 being Neighbourhood of x0 such that

A7: N2 c= N and

A8: N2 c= N1 by RCOMP_1:17;

A9: N2 c= dom (SVF1 (1,f,z0)) by A2, A7;

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

let c be constant Real_Sequence; :: thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) ) )

assume that

A10: rng c = {((proj (1,2)) . z0)} and

A11: rng (h + c) c= N ; :: thesis: ( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

consider g being Real such that

A12: 0 < g and

A13: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;

( x0 + 0 < x0 + g & x0 - g < x0 - 0 ) by A12, XREAL_1:8, XREAL_1:44;

then A14: x0 in N2 by A13;

A15: rng c c= dom (SVF1 (1,f,z0))

( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

rng (c ^\ n) c= N2 and

A22: rng ((h + c) ^\ n) c= N2 ;

consider L being LinearFunc, R being RestFunc such that

A23: for x being Real st x in N1 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;

A24: rng (c ^\ n) c= dom (SVF1 (1,f,z0))

A27: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )

A38: rng (h + c) c= dom (SVF1 (1,f,z0)) by A11, A2;

A39: for k being Element of NAT holds ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

then A43: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (1,f,z0)) /* (h + c)) ^\ n) - ((SVF1 (1,f,z0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A38, VALUED_0:27

.= ((((SVF1 (1,f,z0)) /* (h + c)) ^\ n) - (((SVF1 (1,f,z0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A15, VALUED_0:27

.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17

.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18

.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;

then A44: L . 1 = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) by A27, SEQ_4:22;

thus (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent by A27, A43, SEQ_4:21; :: thesis: partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)))

for x being Real st x in N2 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A23, A8;

hence partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) by A1, A3, A9, A44, Th11; :: thesis: verum

for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

let z0 be Element of REAL 2; :: thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

let N be Neighbourhood of (proj (1,2)) . z0; :: thesis: ( f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) implies for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) ) )

assume that

A1: f is_partial_differentiable_in z0,1 and

A2: N c= dom (SVF1 (1,f,z0)) ; :: thesis: for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

consider x0, y0 being Real such that

A3: z0 = <*x0,y0*> and

A4: ex N1 being Neighbourhood of x0 st

( N1 c= dom (SVF1 (1,f,z0)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Th9;

consider N1 being Neighbourhood of x0 such that

N1 c= dom (SVF1 (1,f,z0)) and

A5: ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N1 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;

A6: (proj (1,2)) . z0 = x0 by A3, Th1;

then consider N2 being Neighbourhood of x0 such that

A7: N2 c= N and

A8: N2 c= N1 by RCOMP_1:17;

A9: N2 c= dom (SVF1 (1,f,z0)) by A2, A7;

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

let c be constant Real_Sequence; :: thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) ) )

assume that

A10: rng c = {((proj (1,2)) . z0)} and

A11: rng (h + c) c= N ; :: thesis: ( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )

consider g being Real such that

A12: 0 < g and

A13: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;

( x0 + 0 < x0 + g & x0 - g < x0 - 0 ) by A12, XREAL_1:8, XREAL_1:44;

then A14: x0 in N2 by A13;

A15: rng c c= dom (SVF1 (1,f,z0))

proof

ex n being Element of NAT st
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom (SVF1 (1,f,z0)) )

assume y in rng c ; :: thesis: y in dom (SVF1 (1,f,z0))

then y = x0 by A10, A6, TARSKI:def 1;

then y in N by A7, A14;

hence y in dom (SVF1 (1,f,z0)) by A2; :: thesis: verum

end;assume y in rng c ; :: thesis: y in dom (SVF1 (1,f,z0))

then y = x0 by A10, A6, TARSKI:def 1;

then y in N by A7, A14;

hence y in dom (SVF1 (1,f,z0)) by A2; :: thesis: verum

( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

proof

then consider n being Element of NAT such that
x0 in rng c
by A10, A6, TARSKI:def 1;

then A16: lim c = x0 by SEQ_4:25;

lim h = 0 ;

then lim (h + c) = 0 + x0 by A16, SEQ_2:6

.= x0 ;

then consider n being Nat such that

A17: for m being Nat st n <= m holds

|.(((h + c) . m) - x0).| < g by A12, SEQ_2:def 7;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

A18: rng (c ^\ n) = {x0} by A10, A6, VALUED_0:26;

thus rng (c ^\ n) c= N2 by A14, A18, TARSKI:def 1; :: thesis: rng ((h + c) ^\ n) c= N2

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )

assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2

then consider m being Element of NAT such that

A19: y = ((h + c) ^\ n) . m by FUNCT_2:113;

n + 0 <= n + m by XREAL_1:7;

then A20: |.(((h + c) . (n + m)) - x0).| < g by A17;

then ((h + c) . (m + n)) - x0 < g by SEQ_2:1;

then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def 3;

then A21: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;

- g < ((h + c) . (m + n)) - x0 by A20, SEQ_2:1;

then - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def 3;

then x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;

hence y in N2 by A13, A19, A21; :: thesis: verum

end;then A16: lim c = x0 by SEQ_4:25;

lim h = 0 ;

then lim (h + c) = 0 + x0 by A16, SEQ_2:6

.= x0 ;

then consider n being Nat such that

A17: for m being Nat st n <= m holds

|.(((h + c) . m) - x0).| < g by A12, SEQ_2:def 7;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

A18: rng (c ^\ n) = {x0} by A10, A6, VALUED_0:26;

thus rng (c ^\ n) c= N2 by A14, A18, TARSKI:def 1; :: thesis: rng ((h + c) ^\ n) c= N2

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )

assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2

then consider m being Element of NAT such that

A19: y = ((h + c) ^\ n) . m by FUNCT_2:113;

n + 0 <= n + m by XREAL_1:7;

then A20: |.(((h + c) . (n + m)) - x0).| < g by A17;

then ((h + c) . (m + n)) - x0 < g by SEQ_2:1;

then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def 3;

then A21: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;

- g < ((h + c) . (m + n)) - x0 by A20, SEQ_2:1;

then - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def 3;

then x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;

hence y in N2 by A13, A19, A21; :: thesis: verum

rng (c ^\ n) c= N2 and

A22: rng ((h + c) ^\ n) c= N2 ;

consider L being LinearFunc, R being RestFunc such that

A23: for x being Real st x in N1 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;

A24: rng (c ^\ n) c= dom (SVF1 (1,f,z0))

proof

A26:
L is total
by FDIFF_1:def 3;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom (SVF1 (1,f,z0)) )

assume A25: y in rng (c ^\ n) ; :: thesis: y in dom (SVF1 (1,f,z0))

rng (c ^\ n) = rng c by VALUED_0:26;

then y = x0 by A10, A6, A25, TARSKI:def 1;

then y in N by A7, A14;

hence y in dom (SVF1 (1,f,z0)) by A2; :: thesis: verum

end;assume A25: y in rng (c ^\ n) ; :: thesis: y in dom (SVF1 (1,f,z0))

rng (c ^\ n) = rng c by VALUED_0:26;

then y = x0 by A10, A6, A25, TARSKI:def 1;

then y in N by A7, A14;

hence y in dom (SVF1 (1,f,z0)) by A2; :: thesis: verum

A27: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )

proof

A37:
rng ((h + c) ^\ n) c= dom (SVF1 (1,f,z0))
by A22, A7, A2;
deffunc H_{1}( Nat) -> set = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);

consider s1 being Real_Sequence such that

A28: for k being Nat holds s1 . k = H_{1}(k)
from SEQ_1:sch 1();

A33: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def 3;

A34: L . 1 = s * 1 by A33

.= s ;

hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A29, SEQ_2:def 6; :: thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1

hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A36, A29, SEQ_2:def 7; :: thesis: verum

end;consider s1 being Real_Sequence such that

A28: for k being Nat holds s1 . k = H

A29: now :: thesis: for r being Real st 0 < r holds

ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

consider s being Real such that ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

A30:
( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 )
by FDIFF_1:def 2;

let r be Real; :: thesis: ( 0 < r implies ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r )

assume 0 < r ; :: thesis: ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

then consider m being Nat such that

A31: for k being Nat st m <= k holds

|.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| < r by A30, SEQ_2:def 7;

take n1 = m; :: thesis: for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

let k be Nat; :: thesis: ( n1 <= k implies |.((s1 . k) - (L . 1)).| < r )

assume A32: n1 <= k ; :: thesis: |.((s1 . k) - (L . 1)).| < r

|.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)).| by A28

.= |.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| ;

hence |.((s1 . k) - (L . 1)).| < r by A31, A32; :: thesis: verum

end;let r be Real; :: thesis: ( 0 < r implies ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r )

assume 0 < r ; :: thesis: ex n1 being Nat st

for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

then consider m being Nat such that

A31: for k being Nat st m <= k holds

|.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| < r by A30, SEQ_2:def 7;

take n1 = m; :: thesis: for k being Nat st n1 <= k holds

|.((s1 . k) - (L . 1)).| < r

let k be Nat; :: thesis: ( n1 <= k implies |.((s1 . k) - (L . 1)).| < r )

assume A32: n1 <= k ; :: thesis: |.((s1 . k) - (L . 1)).| < r

|.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)).| by A28

.= |.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| ;

hence |.((s1 . k) - (L . 1)).| < r by A31, A32; :: thesis: verum

A33: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def 3;

A34: L . 1 = s * 1 by A33

.= s ;

now :: thesis: for m being Element of NAT holds (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m

then A36:
((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1
by FUNCT_2:63;let m be Element of NAT ; :: thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m

A35: (h ^\ n) . m <> 0 by SEQ_1:5;

thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10

.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A26, FUNCT_2:115

.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A33

.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)

.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A35, XCMPLX_0:def 7

.= s1 . m by A28, A34 ; :: thesis: verum

end;A35: (h ^\ n) . m <> 0 by SEQ_1:5;

thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8

.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10

.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A26, FUNCT_2:115

.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A33

.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)

.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A35, XCMPLX_0:def 7

.= s1 . m by A28, A34 ; :: thesis: verum

hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A29, SEQ_2:def 6; :: thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1

hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A36, A29, SEQ_2:def 7; :: thesis: verum

A38: rng (h + c) c= dom (SVF1 (1,f,z0)) by A11, A2;

A39: for k being Element of NAT holds ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

proof

A42:
R is total
by FDIFF_1:def 2;
let k be Element of NAT ; :: thesis: ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;

then A40: ((h + c) ^\ n) . k in N2 by A22;

( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;

then A41: (c ^\ n) . k = x0 by A10, A6, TARSKI:def 1;

(((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15

.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7

.= (h ^\ n) . k ;

hence ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A23, A8, A40, A41; :: thesis: verum

end;((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;

then A40: ((h + c) ^\ n) . k in N2 by A22;

( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;

then A41: (c ^\ n) . k = x0 by A10, A6, TARSKI:def 1;

(((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15

.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7

.= (h ^\ n) . k ;

hence ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A23, A8, A40, A41; :: thesis: verum

now :: thesis: for k being Element of NAT holds (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k

then
((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))
by FUNCT_2:63;let k be Element of NAT ; :: thesis: (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k

thus (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n))) . k = (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (1,f,z0)) /* (c ^\ n)) . k) by RFUNCT_2:1

.= ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - (((SVF1 (1,f,z0)) /* (c ^\ n)) . k) by A37, FUNCT_2:108

.= ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) by A24, FUNCT_2:108

.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A39

.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A26, FUNCT_2:115

.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A42, FUNCT_2:115

.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; :: thesis: verum

end;thus (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n))) . k = (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (1,f,z0)) /* (c ^\ n)) . k) by RFUNCT_2:1

.= ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - (((SVF1 (1,f,z0)) /* (c ^\ n)) . k) by A37, FUNCT_2:108

.= ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) by A24, FUNCT_2:108

.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A39

.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A26, FUNCT_2:115

.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A42, FUNCT_2:115

.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; :: thesis: verum

then A43: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (1,f,z0)) /* (h + c)) ^\ n) - ((SVF1 (1,f,z0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A38, VALUED_0:27

.= ((((SVF1 (1,f,z0)) /* (h + c)) ^\ n) - (((SVF1 (1,f,z0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A15, VALUED_0:27

.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17

.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18

.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;

then A44: L . 1 = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) by A27, SEQ_4:22;

thus (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent by A27, A43, SEQ_4:21; :: thesis: partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)))

for x being Real st x in N2 holds

((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A23, A8;

hence partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) by A1, A3, A9, A44, Th11; :: thesis: verum