let S, T be 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:

reconsider c = NAT --> x0 as sequence of S ;
assume A3: for h being non-zero 0 -convergent 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 object ; :: thesis:
assume x in {x0} ; :: thesis:
then x = x0 by TARSKI:def 1;
then x = c . 1 ;
hence x in rng c by NFCONT_1:6; :: thesis:

end;

then A4: {x0} c= rng c ;

now :: thesis:

let x be object ; :: thesis:
assume x in rng c ; :: thesis:
then consider n being Nat such that
A5: x = c . n by NFCONT_1:6;
n in NAT by ORDINAL1:def 12;
then x = x0 by FUNCOP_1:7, A5;
hence x in {x0} by TARSKI:def 1; :: thesis:

end;

then rng c c= {x0} ;
then A6: 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
( |.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
A7: r > 0 and
A8: for d being Real st d > 0 holds
ex h being Real st
( |.h.| < d & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) ;
defpred S₁[ Nat, Real] means ex rr being Real st
( rr = $2 & |.rr.| < 1 / ($1 + 1) & rr <> 0 & (rr * z) + x0 in N & not ||.(((rr ") * ((f /. ((rr * z) + x0)) - (f /. x0))) - dv).|| < r );
A9: for n being Element of NAT ex h being Element of REAL st S₁[n,h]

proof

let n be Element of NAT ; :: thesis:
0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
then consider h being Real such that
A10: ( |.h.| < 1 / (n + 1) & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) by A8;
h in REAL by XREAL_0:def 1;
hence ex h being Element of REAL st S₁[n,h] by A10; :: thesis:

end;

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

A12: now :: thesis:

let p be Real; :: thesis:
assume A13: 0 < p ; :: thesis:
consider n being Nat such that
A14: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A14, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A13, XREAL_1:76;
then A15: 1 / (n + 1) < p by XCMPLX_1:216;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then A16: n + 1 <= m + 1 by XREAL_1:6;
m in NAT by ORDINAL1:def 12;
then A17: S₁[m,h . m] by A11;
1 / (m + 1) <= 1 / (n + 1) by A16, XREAL_1:118;
then |.((h . m) - 0).| < 1 / (n + 1) by A17, XXREAL_0:2;
hence |.((h . m) - 0).| < p by A15, XXREAL_0:2; :: thesis:

end;

then A18: h is convergent by SEQ_2:def 6;
then A19: lim h = 0 by A12, SEQ_2:def 7;
for n being Nat holds h . n <> 0

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then S₁[n,h . n] by A11;
hence h . n <> 0 ; :: thesis:

end;

then h is non-zero by SEQ_1:5;
then reconsider h = h as non-zero 0 -convergent Real_Sequence by A18, A19, FDIFF_1:def 1;

now :: thesis:

let x be object ; :: thesis:
assume x in rng ((h * z) + c) ; :: thesis:
then consider n being Nat such that
A20: x = ((h * z) + c) . n by NFCONT_1:6;
A21: n in NAT by ORDINAL1:def 12;
A22: x = ((h * z) . n) + (c . n) by A20, NORMSP_1:def 2
.= ((h . n) * z) + (c . n) by NDIFF_1:def 3
.= ((h . n) * z) + x0 by FUNCOP_1:7, A21 ;
S₁[n,h . n] by A11, A21;
hence x in N by A22; :: thesis:

end;

then A23: rng ((h * z) + c) c= N ;
then ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A3, A6;
then consider n being Nat such that
A24: for m being Nat st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A7, NORMSP_1:def 7;
x0 in N by NFCONT_1:4;
then A25: rng c c= dom f by A1, A6, ZFMISC_1:31;
A26: n in NAT by ORDINAL1:def 12;
A27: S₁[n,h . n] by A11, A26;
||.((((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 A25, FUNCT_2:109, A26
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - (f /. x0))) - dv).|| by FUNCOP_1:7, A26
.= ||.((((h . n) ") * ((f /. (((h * z) + c) . n)) - (f /. x0))) - dv).|| by A1, A23, FUNCT_2:109, A26, 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, A26
.= ||.((((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 |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) by A24, A27; :: thesis:

end;

now :: thesis:

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

now :: thesis:

let h be non-zero 0 -convergent Real_Sequence; :: thesis:
let c be constant sequence of S; :: thesis:
assume that
A29: rng c = {x0} and
A30: rng ((h * z) + c) c= N ; :: thesis:
A31: ( h is convergent & lim h = 0 ) ;
x0 in N by NFCONT_1:4;
then A32: rng c c= dom f by A1, A29, ZFMISC_1:31;
A33: 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 A29, TARSKI:def 1; :: thesis:

end;

A34: now :: thesis:

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider d being Real such that
A35: d > 0 and
A36: for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r by A28;
consider n being Nat such that
A37: for m being Nat st n <= m holds
|.((h . m) - 0).| < d by A31, A35, SEQ_2:def 7;
take n = n; :: thesis:
thus for m being Nat st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r :: thesis:

proof

let m be Nat; :: thesis:
A38: m in NAT by ORDINAL1:def 12;
A39: h . m <> 0 by SEQ_1:5;
assume n <= m ; :: thesis:
then A40: |.((h . m) - 0).| < d by A37;
((h * z) + c) . m in rng ((h * z) + c) by NFCONT_1:6;
then ((h * z) + c) . m in N by A30;
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 A41: ((h . m) * z) + x0 in N by A33, A38;
||.((((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 A32, FUNCT_2:109, A38
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - (f /. x0))) - dv).|| by A33, A38
.= ||.((((h . m) ") * ((f /. (((h * z) + c) . m)) - (f /. x0))) - dv).|| by A1, A30, FUNCT_2:109, XBOOLE_1:1, A38
.= ||.((((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 A33, A38
.= ||.((((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 A36, A40, A39, A41; :: 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 A34, NORMSP_1:def 7; :: thesis:

end;

hence for h being non-zero 0 -convergent 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 non-zero 0 -convergent 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 |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) by A2; :: thesis: