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

assume A3: for h being convergent_to_0 Real_Sequence
for c being V8() 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:
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
A4: r > 0 and
A5: 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 );
A6: 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 + 0 < 1 + n ;
then 0 < 1 * ((n + 1) " ) ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
then consider h being Real such that
A7: ( abs h < 1 / (n + 1) & h <> 0 & (h * z) + x0 in N & not ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) by A5;
thus ex h being Real st S₁[n,h] by A7; :: thesis:

end;

consider h being Real_Sequence such that
A8: for n being Element of NAT holds S₁[n,h . n] from FUNCT_2:sch 3(A6);
reconsider c = NAT --> x0 as sequence of S ;
A9: rng c = {x0}

proof

now

let x be set ; :: thesis:
assume x in rng c ; :: thesis:
then consider n being Element of NAT such that
A10: x = c . n by NFCONT_1:6;
x = x0 by A10, FUNCOP_1:13;
hence x in {x0} by TARSKI:def 1; :: thesis:

end;

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

now

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

end;

then {x0} c= rng c by TARSKI:def 3;
hence rng c = {x0} by A11, XBOOLE_0:def 10; :: thesis:

end;

x0 in N by NFCONT_1:4;
then A12: rng c c= dom f by A1, A9, ZFMISC_1:37;

A13: now

let p be real number ; :: thesis:
assume 0 < p ; :: thesis:
then A14: 0 < p " ;
consider n being Element of NAT such that
A15: p " < n by SEQ_4:10;
(p " ) + 0 < n + 1 by A15, XREAL_1:10;
then 1 / (n + 1) < 1 / (p " ) by A14, XREAL_1:78;
then A16: 1 / (n + 1) < p by XCMPLX_1:218;
take n = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A17: n + 1 <= m + 1 by XREAL_1:8;
0 <= n by NAT_1:2;
then 0 + 0 < 1 + n ;
then A18: 1 / (m + 1) <= 1 / (n + 1) by A17, XREAL_1:120;
S₁[m,h . m] by A8;
then abs ((h . m) - 0 ) < 1 / (n + 1) by A18, XXREAL_0:2;
hence abs ((h . m) - 0 ) < p by A16, XXREAL_0:2; :: thesis:

end;

then A19: h is convergent by SEQ_2:def 6;
then A20: lim h = 0 by A13, 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 A8;
hence h . n <> 0 ; :: thesis:

end;

then h is non-zero by SEQ_1:7;
then reconsider h = h as convergent_to_0 Real_Sequence by A19, A20, FDIFF_1:def 1;
A21: rng ((h * z) + c) c= N

proof

now

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

end;

hence rng ((h * z) + c) c= N by TARSKI:def 3; :: thesis:

end;

then ( (h " ) (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A3, A9;
then consider n being Element of NAT such that
A24: for m being Element of NAT st n <= m holds
||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A4, NORMSP_1:def 11;
A25: S₁[n,h . n] by A8;
||.((((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 6
.= ||.((((h . n) " ) * (((f /* ((h * z) + c)) . n) - (f /. (c . n)))) - dv).|| by A12, FUNCT_2:186
.= ||.((((h . n) " ) * (((f /* ((h * z) + c)) . n) - (f /. x0))) - dv).|| by FUNCOP_1:13
.= ||.((((h . n) " ) * ((f /. (((h * z) + c) . n)) - (f /. x0))) - dv).|| by A1, A21, FUNCT_2:186, XBOOLE_1:1
.= ||.((((h . n) " ) * ((f /. (((h * z) . n) + (c . n))) - (f /. x0))) - dv).|| by NORMSP_1:def 5
.= ||.((((h . n) " ) * ((f /. (((h * z) . n) + x0)) - (f /. x0))) - dv).|| by FUNCOP_1:13
.= ||.((((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 A24, A25; :: thesis:

end;

now

assume A26: 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 V8() sequence of S; :: thesis:
assume that
A27: rng c = {x0} and
A28: rng ((h * z) + c) c= N ; :: thesis:
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 A27, TARSKI:def 1; :: thesis:

end;

x0 in N by NFCONT_1:4;
then A30: rng c c= dom f by A1, A27, ZFMISC_1:37;
A31: h is non-zero by FDIFF_1:def 1;
A32: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;

A33: now

let r be Real; :: thesis:
assume A34: r > 0 ; :: thesis:
consider d being Real such that
A35: d > 0 and
A36: 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 A26, A34;
consider n being Element of NAT such that
A37: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < d by A32, A35, 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:
assume n <= m ; :: thesis:
then A38: abs ((h . m) - 0 ) < d by A37;
A39: h . m <> 0 by A31, SEQ_1:7;
((h * z) + c) . m in rng ((h * z) + c) by NFCONT_1:6;
then ((h * z) + c) . m in N by A28;
then ((h * z) . m) + (c . m) in N by NORMSP_1:def 5;
then ((h . m) * z) + (c . m) in N by NDIFF_1:def 3;
then A40: ((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 6
.= ||.((((h . m) " ) * (((f /* ((h * z) + c)) . m) - (f /. (c . m)))) - dv).|| by A30, FUNCT_2:186
.= ||.((((h . m) " ) * (((f /* ((h * z) + c)) . m) - (f /. x0))) - dv).|| by A29
.= ||.((((h . m) " ) * ((f /. (((h * z) + c) . m)) - (f /. x0))) - dv).|| by A1, A28, FUNCT_2:186, XBOOLE_1:1
.= ||.((((h . m) " ) * ((f /. (((h * z) . m) + (c . m))) - (f /. x0))) - dv).|| by NORMSP_1:def 5
.= ||.((((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 A36, A38, A39, A40; :: thesis:

end;

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

end;

hence for h being convergent_to_0 Real_Sequence
for c being V8() 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 V8() 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: