let S, T be non trivial RealNormSpace; :: thesis:
let f be PartFunc of S,T; :: thesis:
let x0 be Point of S; :: thesis:
let N be Neighbourhood of x0; :: thesis:
assume A1: N c= dom f ; :: thesis:
let z be Point of S; :: thesis:
let dv be Point of T; :: thesis:

A2: now

reconsider c = NAT --> x0 as sequence of S ;
assume A3: for h being convergent_to_0 Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ; :: thesis:

let x be set ; :: thesis:
assume x in {x0} ; :: thesis:
then x = x0 by TARSKI:def 1;
then x = c . 1 by FUNCOP_1:7;
hence x in rng c by NFCONT_1:6; :: thesis:

end;

then A4: {x0} c= rng c by TARSKI:def 3;

now

let x be set ; :: thesis:
assume x in rng c ; :: thesis:
then ex n being Element of NAT st x = c . n by NFCONT_1:6;
then x = x0 by FUNCOP_1:7;
hence x in {x0} by TARSKI:def 1; :: thesis:

end;

then rng c c= {x0} by TARSKI:def 3;
then A5: rng c = {x0} by A4, XBOOLE_0:def 10;
assume ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex h being Real st
( abs h < d & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) ) ) ) ; :: thesis:
then consider r being Real such that
A6: r > 0 and
A7: for d being Real st d > 0 holds
ex h being Real st
( abs h < d & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) ;
defpred S₁[ Nat, real number ] means ex rr being Real st
( rr = $2 & abs rr < 1 / ($1 + 1) & rr <> 0 & (rr * z) + x0 in N & not ||.(((rr ") * ((f /. ((rr * z) + x0)) - (f /. x0))) - dv).|| < r );
A8: for n being Element of NAT ex h being Real st S₁[n,h]

proof

let n be Element of NAT ; :: thesis:
0 <= n by NAT_1:2;
then 0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
then ex h being Real st
( abs h < 1 / (n + 1) & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) by A7;
hence ex h being Real st S₁[n,h] ; :: thesis:

end;

consider h being Real_Sequence such that
A9: for n being Element of NAT holds S₁[n,h . n] from FUNCT_2:sch 3(A8);

A10: now

let p be real number ; :: thesis:
assume A11: 0 < p ; :: thesis:
consider n being Element of NAT such that
A12: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A12, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A11, XREAL_1:76;
then A13: 1 / (n + 1) < p by XCMPLX_1:216;
take n = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A14: n + 1 <= m + 1 by XREAL_1:6;
A15: S₁[m,h . m] by A9;
0 <= n by NAT_1:2;
then 1 / (m + 1) <= 1 / (n + 1) by A14, XREAL_1:118;
then abs ((h . m) - 0) < 1 / (n + 1) by A15, XXREAL_0:2;
hence abs ((h . m) - 0) < p by A13, XXREAL_0:2; :: thesis:

end;

then A16: h is convergent by SEQ_2:def 6;
then A17: lim h = 0 by A10, SEQ_2:def 7;
for n being Element of NAT holds h . n <> 0

proof

let n be Element of NAT ; :: thesis:
S₁[n,h . n] by A9;
hence h . n <> 0 ; :: thesis:

end;

then h is non-empty by SEQ_1:5;
then reconsider h = h as convergent_to_0 Real_Sequence by A16, A17, FDIFF_1:def 1;

now

let x be set ; :: thesis:
assume x in rng ((h * z) + c) ; :: thesis:
then consider n being Element of NAT such that
A18: x = ((h * z) + c) . n by NFCONT_1:6;
A19: x = ((h * z) . n) + (c . n) by A18, NORMSP_1:def 2
.= ((h . n) * z) + (c . n) by NDIFF_1:def 3
.= ((h . n) * z) + x0 by FUNCOP_1:7 ;
S₁[n,h . n] by A9;
hence x in N by A19; :: thesis:

end;

then A20: rng ((h * z) + c) c= N by TARSKI:def 3;
then ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A3, A5;
then consider n being Element of NAT such that
A21: for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A6, NORMSP_1:def 7;
x0 in N by NFCONT_1:4;
then A22: rng c c= dom f by A1, A5, ZFMISC_1:31;
A23: S₁[n,h . n] by A9;
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - dv).|| = ||.((((h ") . n) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - dv).|| by NDIFF_1:def 2
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) - (f /* c)) . n)) - dv).|| by VALUED_1:10
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - ((f /* c) . n))) - dv).|| by NORMSP_1:def 3
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - (f /. (c . n)))) - dv).|| by A22, FUNCT_2:109
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - (f /. x0))) - dv).|| by FUNCOP_1:7
.= ||.((((h . n) ") * ((f /. (((h * z) + c) . n)) - (f /. x0))) - dv).|| by A1, A20, FUNCT_2:109, XBOOLE_1:1
.= ||.((((h . n) ") * ((f /. (((h * z) . n) + (c . n))) - (f /. x0))) - dv).|| by NORMSP_1:def 2
.= ||.((((h . n) ") * ((f /. (((h * z) . n) + x0)) - (f /. x0))) - dv).|| by FUNCOP_1:7
.= ||.((((h . n) ") * ((f /. (((h . n) * z) + x0)) - (f /. x0))) - dv).|| by NDIFF_1:def 3 ;
hence for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) by A21, A23; :: thesis:

end;

now

assume A24: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ; :: thesis:

now

let h be convergent_to_0 Real_Sequence; :: thesis:
let c be constant sequence of S; :: thesis:
assume that
A25: rng c = {x0} and
A26: rng ((h * z) + c) c= N ; :: thesis:
A27: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
x0 in N by NFCONT_1:4;
then A28: rng c c= dom f by A1, A25, ZFMISC_1:31;
A29: for n being Element of NAT holds c . n = x0

proof

let n be Element of NAT ; :: thesis:
c . n in rng c by NFCONT_1:6;
hence c . n = x0 by A25, TARSKI:def 1; :: thesis:

end;

A30: h is non-empty by FDIFF_1:def 1;

A31: now

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider d being Real such that
A32: d > 0 and
A33: for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r by A24;
consider n being Element of NAT such that
A34: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < d by A27, A32, SEQ_2:def 7;
take n = n; :: thesis:
thus for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r :: thesis:

proof

let m be Element of NAT ; :: thesis:
A35: h . m <> 0 by A30, SEQ_1:5;
assume n <= m ; :: thesis:
then A36: abs ((h . m) - 0) < d by A34;
((h * z) + c) . m in rng ((h * z) + c) by NFCONT_1:6;
then ((h * z) + c) . m in N by A26;
then ((h * z) . m) + (c . m) in N by NORMSP_1:def 2;
then ((h . m) * z) + (c . m) in N by NDIFF_1:def 3;
then A37: ((h . m) * z) + x0 in N by A29;
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| = ||.((((h ") . m) * (((f /* ((h * z) + c)) - (f /* c)) . m)) - dv).|| by NDIFF_1:def 2
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) - (f /* c)) . m)) - dv).|| by VALUED_1:10
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - ((f /* c) . m))) - dv).|| by NORMSP_1:def 3
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - (f /. (c . m)))) - dv).|| by A28, FUNCT_2:109
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - (f /. x0))) - dv).|| by A29
.= ||.((((h . m) ") * ((f /. (((h * z) + c) . m)) - (f /. x0))) - dv).|| by A1, A26, FUNCT_2:109, XBOOLE_1:1
.= ||.((((h . m) ") * ((f /. (((h * z) . m) + (c . m))) - (f /. x0))) - dv).|| by NORMSP_1:def 2
.= ||.((((h . m) ") * ((f /. (((h * z) . m) + x0)) - (f /. x0))) - dv).|| by A29
.= ||.((((h . m) ") * ((f /. (((h . m) * z) + x0)) - (f /. x0))) - dv).|| by NDIFF_1:def 3 ;
hence ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A33, A36, A35, A37; :: thesis:

end;

hence (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent by NORMSP_1:def 6; :: thesis:
hence lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = dv by A31, NORMSP_1:def 7; :: thesis:

end;

hence for h being convergent_to_0 Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ; :: thesis:

end;

hence ( ( for h being convergent_to_0 Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) by A2; :: thesis: