let f be PartFunc of (REAL 3),REAL; :: thesis:
let u0 be Element of REAL 3; :: thesis:
let N be Neighbourhood of (proj (1,3)) . u0; :: thesis:
assume A1: ( f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) ) ; :: thesis:
let h be non-zero 0 -convergent Real_Sequence; :: thesis:
let c be constant Real_Sequence; :: thesis:
assume A2: ( rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N ) ; :: thesis:
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of x0 st
( N1 c= dom (SVF1 (1,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A1, Th13;
consider N1 being Neighbourhood of x0 such that
A4: ( N1 c= dom (SVF1 (1,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A3;
consider L being LinearFunc, R being RestFunc such that
A5: for x being Real st x in N1 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
A6: (proj (1,3)) . u0 = x0 by A3, Th1;
then consider N2 being Neighbourhood of x0 such that
A7: ( N2 c= N & N2 c= N1 ) by RCOMP_1:17;
consider g being Real such that
A8: ( 0 < g & N2 = ].(x0 - g),(x0 + g).[ ) by RCOMP_1:def 6;
A9: x0 in N2

A10: x0 + 0 < x0 + g by A8, XREAL_1:8;
x0 - g < x0 - 0 by A8, XREAL_1:44;
hence x0 in N2 by A8, A10; :: thesis:

end;

ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

proof

x0 in rng c by A2, A6, TARSKI:def 1;
then A11: lim c = x0 by SEQ_4:25;
( h is convergent & lim h = 0 ) ;
then A12: lim (h + c) = 0 + x0 by A11, SEQ_2:6
.= x0 ;
consider n being Nat such that
A13: for m being Nat st n <= m holds
|.(((h + c) . m) - x0).| < g by A8, A12, SEQ_2:def 7;
A14: rng (c ^\ n) = {x0} by A2, A6, VALUED_0:26;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis:
thus rng (c ^\ n) c= N2 by A9, A14, TARSKI:def 1; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((h + c) ^\ n) ; :: thesis:
then consider m being Element of NAT such that
A15: y = ((h + c) ^\ n) . m by FUNCT_2:113;
n + 0 <= n + m by XREAL_1:7;
then |.(((h + c) . (n + m)) - x0).| < g by A13;
then ( - g < ((h + c) . (m + n)) - x0 & ((h + c) . (m + n)) - x0 < g ) by SEQ_2:1;
then ( - g < (((h + c) ^\ n) . m) - x0 & (((h + c) ^\ n) . m) - x0 < g ) by NAT_1:def 3;
then ( x0 + (- g) < ((h + c) ^\ n) . m & ((h + c) ^\ n) . m < x0 + g ) by XREAL_1:19, XREAL_1:20;
hence y in N2 by A8, A15; :: thesis:

end;

then consider n being Element of NAT such that
A16: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) ;
A17: rng (c ^\ n) c= dom (SVF1 (1,f,u0))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
A18: rng (c ^\ n) = rng c by VALUED_0:26;
assume y in rng (c ^\ n) ; :: thesis:
then y = x0 by A2, A6, A18, TARSKI:def 1;
then y in N by A7, A9;
hence y in dom (SVF1 (1,f,u0)) by A1; :: thesis:

end;

A19: rng ((h + c) ^\ n) c= dom (SVF1 (1,f,u0)) by A16, A7, A1;
A20: rng c c= dom (SVF1 (1,f,u0))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng c ; :: thesis:
then y = x0 by A2, A6, TARSKI:def 1;
then y in N by A7, A9;
hence y in dom (SVF1 (1,f,u0)) by A1; :: thesis:

end;

A21: rng (h + c) c= dom (SVF1 (1,f,u0)) by A2, A1;
A22: for x being Real st x in N2 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5, A7;
A23: for k being Element of NAT holds ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))

proof

let k be Element of NAT ; :: thesis:
((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;
then A24: ((h + c) ^\ n) . k in N2 by A16;
A25: (((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 ;
A26: (c ^\ n) . k in rng (c ^\ n) by VALUED_0:28;
rng (c ^\ n) = rng c by VALUED_0:26;
then (c ^\ n) . k = x0 by A2, A6, A26, TARSKI:def 1;
hence ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A5, A7, A24, A25; :: thesis:

end;

A27: L is total by FDIFF_1:def 3;
A28: R is total by FDIFF_1:def 2;
A29: ((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))

proof

now :: thesis:

let k be Element of NAT ; :: thesis:
thus (((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n))) . k = (((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (1,f,u0)) /* (c ^\ n)) . k) by RFUNCT_2:1
.= ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - (((SVF1 (1,f,u0)) /* (c ^\ n)) . k) by A19, FUNCT_2:108
.= ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) by A17, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A23
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A27, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A28, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; :: thesis:

end;

hence ((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63; :: thesis:

end;

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

proof

deffunc H₁( Nat) -> set = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Real_Sequence such that
A31: for k being Nat holds s1 . k = H₁(k) from SEQ_1:sch 1();
consider s being Real such that
A32: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def 3;
A33: L . 1 = s * 1 by A32
.= s ;

now :: thesis:

let m be Element of NAT ; :: thesis:
A34: (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 A27, FUNCT_2:115
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A34, XCMPLX_0:def 7
.= s1 . m by A31, A33 ; :: thesis:

end;

then A35: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;

A36: now :: thesis:

let r be Real; :: thesis:
assume A37: 0 < r ; :: thesis:
( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def 2;
then consider m being Nat such that
A38: for k being Nat st m <= k holds
|.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| < r by A37, SEQ_2:def 7;
take n1 = m; :: thesis:
let k be Nat; :: thesis:
assume A39: n1 <= k ; :: thesis:
|.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)).| by A31
.= |.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0).| ;
hence |.((s1 . k) - (L . 1)).| < r by A38, A39; :: thesis:

end;

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

end;

A40: N2 c= dom (SVF1 (1,f,u0)) by A1, A7;
A41: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (1,f,u0)) /* (h + c)) ^\ n) - ((SVF1 (1,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A21, A29, VALUED_0:27
.= ((((SVF1 (1,f,u0)) /* (h + c)) ^\ n) - (((SVF1 (1,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A20, VALUED_0:27
.= ((((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= ((((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= ((((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A42: L . 1 = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) by A30, SEQ_4:22;
thus (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent by A30, A41, SEQ_4:21; :: thesis:
thus partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) by A1, A3, A22, A40, A42, Th16; :: thesis: