let f be PartFunc of (REAL 3),REAL ; :: thesis:
let u0 be Element of REAL 3; :: thesis:
let N be Neighbourhood of (proj 2,3) . u0; :: thesis:
assume A1: ( f is_partial_differentiable_in u0,2 & N c= dom (SVF1 2,f,u0) ) ; :: thesis:
let h be convergent_to_0 Real_Sequence; :: thesis:
let c be V8() Real_Sequence; :: thesis:
assume A2: ( rng c = {((proj 2,3) . u0)} & rng (h + c) c= N ) ; :: thesis:
consider x0, y0, z0 being Real such that
A4: ( u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of y0 st
( N1 c= dom (SVF1 2,f,u0) & ex L being LINEAR ex R being REST st
for y being Real st y in N1 holds
((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A1, BXXLXSDef11;
consider N1 being Neighbourhood of y0 such that
A5: ( N1 c= dom (SVF1 2,f,u0) & ex L being LINEAR ex R being REST st
for y being Real st y in N1 holds
((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A4;
consider L being LINEAR, R being REST such that
A6: for y being Real st y in N1 holds
((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
A7: (proj 2,3) . u0 = y0 by A4, Th2;
consider N2 being Neighbourhood of y0 such that
A8: ( N2 c= N & N2 c= N1 ) by A7, RCOMP_1:38;
consider g being real number such that
A9: ( 0 < g & N2 = ].(y0 - g),(y0 + g).[ ) by RCOMP_1:def 7;
A10: y0 in N2

A11: y0 + 0 < y0 + g by A9, XREAL_1:10;
AA: y0 - g < y0 - 0 by A9, XREAL_1:46;
thus y0 in N2 by A9, A11, AA; :: thesis:

end;

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

proof

y0 in rng c by A2, A7, TARSKI:def 1;
then A13: lim c = y0 by SEQ_4:40;
A14: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
then A15: lim (h + c) = 0 + y0 by A13, SEQ_2:20
.= y0 ;
h + c is convergent by A14, SEQ_2:19;
then consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - y0) < g by A9, A15, SEQ_2:def 7;
A17: rng (c ^\ n) = {y0} by A2, A7, VALUED_0:26;
take n ; :: thesis:
thus rng (c ^\ n) c= N2 :: thesis:

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (c ^\ n) ; :: thesis:
hence y in N2 by A10, A17, TARSKI:def 1; :: thesis:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((h + c) ^\ n) ; :: thesis:
then consider m being Element of NAT such that
A18: y = ((h + c) ^\ n) . m by FUNCT_2:190;
n + 0 <= n + m by XREAL_1:9;
then abs (((h + c) . (n + m)) - y0) < g by A16;
then ( - g < ((h + c) . (m + n)) - y0 & ((h + c) . (m + n)) - y0 < g ) by SEQ_2:9;
then ( - g < (((h + c) ^\ n) . m) - y0 & (((h + c) ^\ n) . m) - y0 < g ) by NAT_1:def 3;
then AB: ( y0 + (- g) < ((h + c) ^\ n) . m & ((h + c) ^\ n) . m < y0 + g ) by XREAL_1:21, XREAL_1:22;
thus y in N2 by A9, A18, AB; :: thesis:

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
A21: rng (c ^\ n) = rng c by VALUED_0:26;
assume y in rng (c ^\ n) ; :: thesis:
then y = y0 by A2, A7, A21, TARSKI:def 1;
then y in N by A8, A10;
hence y in dom (SVF1 2,f,u0) by A1; :: thesis:

end;

A22: rng ((h + c) ^\ n) c= dom (SVF1 2,f,u0)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((h + c) ^\ n) ; :: thesis:
then y in N2 by A19;
then y in N by A8;
hence y in dom (SVF1 2,f,u0) by A1; :: thesis:

end;

A23: rng c c= dom (SVF1 2,f,u0)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng c ; :: thesis:
then y = y0 by A2, A7, TARSKI:def 1;
then y in N by A8, A10;
hence y in dom (SVF1 2,f,u0) by A1; :: thesis:

end;

A24: rng (h + c) c= dom (SVF1 2,f,u0)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (h + c) ; :: thesis:
then y in N by A2;
hence y in dom (SVF1 2,f,u0) by A1; :: thesis:

end;

A25: for y being Real st y in N2 holds
((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0)) by A6, A8;
A26: for k being Element of NAT holds ((SVF1 2,f,u0) . (((h + c) ^\ n) . k)) - ((SVF1 2,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 A27: ((h + c) ^\ n) . k in N2 by A19;
A28: (((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:37
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:11
.= (h ^\ n) . k ;
A29: (c ^\ n) . k in rng (c ^\ n) by VALUED_0:28;
rng (c ^\ n) = rng c by VALUED_0:26;
then (c ^\ n) . k = y0 by A2, A7, A29, TARSKI:def 1;
hence ((SVF1 2,f,u0) . (((h + c) ^\ n) . k)) - ((SVF1 2,f,u0) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A6, A8, A27, A28; :: thesis:

end;

A30: L is total by FDIFF_1:def 4;
A31: R is total by FDIFF_1:def 3;
A32: ((SVF1 2,f,u0) /* ((h + c) ^\ n)) - ((SVF1 2,f,u0) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))

proof

now

let k be Element of NAT ; :: thesis:
thus (((SVF1 2,f,u0) /* ((h + c) ^\ n)) - ((SVF1 2,f,u0) /* (c ^\ n))) . k = (((SVF1 2,f,u0) /* ((h + c) ^\ n)) . k) - (((SVF1 2,f,u0) /* (c ^\ n)) . k) by RFUNCT_2:6
.= ((SVF1 2,f,u0) . (((h + c) ^\ n) . k)) - (((SVF1 2,f,u0) /* (c ^\ n)) . k) by A22, FUNCT_2:185
.= ((SVF1 2,f,u0) . (((h + c) ^\ n) . k)) - ((SVF1 2,f,u0) . ((c ^\ n) . k)) by A20, FUNCT_2:185
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A26
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A30, FUNCT_2:192
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A31, FUNCT_2:192
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:11 ; :: thesis:

end;

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

end;

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

proof

deffunc H₁( Element of NAT ) -> Element of REAL = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . $1);
consider s1 being Real_Sequence such that
A34: for k being Element of NAT holds s1 . k = H₁(k) from SEQ_1:sch 1();
consider s being Real such that
A35: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def 4;
A36: L . 1 = s * 1 by A35
.= s ;

now

let m be Element of NAT ; :: thesis:
h ^\ n is non-empty by FDIFF_1:def 1;
then A37: (h ^\ n) . m <> 0 by SEQ_1:7;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) " ) . m) by SEQ_1:12
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) " ) . m) by SEQ_1:11
.= (((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:12
.= (((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 A30, FUNCT_2:192
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by A35
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) " ))) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by A37, XCMPLX_0:def 7
.= s1 . m by A34, A36 ; :: thesis:

end;

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

A39: now

let r be real number ; :: thesis:
assume A40: 0 < r ; :: thesis:
( ((h ^\ n) " ) (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) " ) (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def 3;
then consider m being Element of NAT such that
A41: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ) < r by A40, SEQ_2:def 7;
take n1 = m; :: thesis:
let k be Element of NAT ; :: thesis:
assume A42: n1 <= k ; :: thesis:
abs ((s1 . k) - (L . 1)) = abs (((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . k)) - (L . 1)) by A34
.= abs (((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ) ;
hence abs ((s1 . k) - (L . 1)) < r by A41, A42; :: thesis:

end;

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

end;

A43: N2 c= dom (SVF1 2,f,u0) by A1, A8, XBOOLE_1:1;
A44: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ) = ((((SVF1 2,f,u0) /* (h + c)) ^\ n) - ((SVF1 2,f,u0) /* (c ^\ n))) (#) ((h ^\ n) " ) by A24, A32, VALUED_0:27
.= ((((SVF1 2,f,u0) /* (h + c)) ^\ n) - (((SVF1 2,f,u0) /* c) ^\ n)) (#) ((h ^\ n) " ) by A23, VALUED_0:27
.= ((((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c)) ^\ n) (#) ((h ^\ n) " ) by SEQM_3:39
.= ((((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c)) ^\ n) (#) ((h " ) ^\ n) by SEQM_3:41
.= ((((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c)) (#) (h " )) ^\ n by SEQM_3:42 ;
then A45: L . 1 = lim ((h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c))) by A33, SEQ_4:36;
thus (h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c)) is convergent by A33, A44, SEQ_4:35; :: thesis:
thus partdiff f,u0,2 = lim ((h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c))) by A1, A4, A25, A43, A45, BXXLXSDef13; :: thesis: