let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let x0 be Point of S; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let N be Neighbourhood of x0; :: thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being convergent_to_0 sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) )
assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f ; :: thesis: for h being convergent_to_0 sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let h be convergent_to_0 sequence of S; :: thesis: for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let c be constant sequence of S; :: thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) )
assume that
A3: rng c = {x0} and
A4: rng (h + c) c= N ; :: thesis: ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A5: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being REST of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= N and
A7: N2 c= N1 by Th1;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being REST of S,T such that
A8: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5;
consider g being Real such that
A9: 0 < g and
A10: { y where y is Point of S : ||.(y - x0).|| < g } c= N2 by NFCONT_1:def 1;
A11: x0 in N2 by NFCONT_1:4;
ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

proof

c . 0 in rng c by NFCONT_1:6;
then c . 0 = x0 by A3, TARSKI:def 1;
then A12: lim c = x0 by Th21;
A13: ( c is convergent & h is convergent ) by Def4, Th21;
then A14: h + c is convergent by NORMSP_1:19;
lim h = 0. S by Def4;
then lim (h + c) = (0. S) + x0 by A12, A13, NORMSP_1:25
.= x0 by RLVECT_1:4 ;
then consider n being Element of NAT such that
A15: for m being Element of NAT st n <= m holds
||.(((h + c) . m) - x0).|| < g by A9, A14, NORMSP_1:def 7;
take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A16: rng (c ^\ n) = {x0} by A3, VALUED_0:26;
thus rng (c ^\ n) c= N2 :: thesis: rng ((h + c) ^\ n) c= N2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in N2 )
assume y in rng (c ^\ n) ; :: thesis: y in N2
hence y in N2 by A11, A16, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2
then consider m being Element of NAT such that
A17: y = ((h + c) ^\ n) . m by NFCONT_1:6;
reconsider y1 = y as Point of S by A17;
0 <= m by NAT_1:2;
then n + 0 <= n + m by XREAL_1:7;
then ||.(((h + c) . (n + m)) - x0).|| < g by A15;
then ||.((((h + c) ^\ n) . m) - x0).|| < g by NAT_1:def 3;
then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A17;
hence y in N2 by A10; :: thesis: verum

end;

then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A18: rng ((h + c) ^\ n) c= N2 ;
A19: lim (h ^\ n) = 0. S by Def4;
A20: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))

proof

let k be Element of NAT ; :: thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
((h + c) ^\ n) . k in rng ((h + c) ^\ n) by NFCONT_1:6;
then A21: ((h + c) ^\ n) . k in N2 by A18;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by NFCONT_1:6, VALUED_0:26;
then A22: (c ^\ n) . k = x0 by A3, TARSKI:def 1;
(((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def 3
.= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by NORMSP_1:def 2
.= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def 3
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def 3
.= ((h ^\ n) . k) + (((c ^\ n) . k) - ((c ^\ n) . k)) by RLVECT_1:def 3
.= ((h ^\ n) . k) + (0. S) by RLVECT_1:15
.= (h ^\ n) . k by RLVECT_1:4 ;
hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A8, A7, A21, A22; :: thesis: verum

end;

R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;
then reconsider L = L as Element of BoundedLinearOperators (S,T) ;
reconsider LP = modetrans (L,S,T) as PartFunc of S,T ;
A23: lim (R /* (h ^\ n)) = 0. T by Th27;
A24: rng ((h + c) ^\ n) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in dom f )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in dom f
then y in N2 by A18;
then y in N by A6;
hence y in dom f by A2; :: thesis: verum

end;

R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 2;
then A25: rng (h ^\ n) c= dom R ;
A26: rng (c ^\ n) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom f )
assume A27: y in rng (c ^\ n) ; :: thesis: y in dom f
rng (c ^\ n) = rng c by VALUED_0:26;
then y = x0 by A3, A27, TARSKI:def 1;
then y in N by NFCONT_1:4;
hence y in dom f by A2; :: thesis: verum

end;

A28: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def 1;
then A29: rng (h ^\ n) c= dom (modetrans (L,S,T)) ;

now

let k be Element of NAT ; :: thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def 3
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A24, FUNCT_2:109
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A26, FUNCT_2:109
.= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A20
.= ((modetrans (L,S,T)) . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by LOPBAN_1:def 11
.= (LP /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A28, PARTFUN1:def 6
.= ((LP /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by A29, FUNCT_2:109
.= ((LP /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A25, FUNCT_2:109
.= ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def 2 ; :: thesis: verum

end;

then A30: (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
A31: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def 1;
LP is_Lipschitzian_on the carrier of S

proof

thus the carrier of S c= dom LP by FUNCT_2:def 1; :: according to NFCONT_1:def 9 :: thesis: ex b₁ being Element of REAL st
( not b₁ <= 0 & ( for b₂, b₃ being Element of the carrier of S holds
( not b₂ in the carrier of S or not b₃ in the carrier of S or ||.((LP /. b₂) - (LP /. b₃)).|| <= b₁ * ||.(b₂ - b₃).|| ) ) )
set LL = modetrans (L,S,T);
consider K being Real such that
A32: 0 <= K and
A33: for x being VECTOR of S holds ||.((modetrans (L,S,T)) . x).|| <= K * ||.x.|| by LOPBAN_1:def 8;
take K + 1 ; :: thesis: ( not K + 1 <= 0 & ( for b₁, b₂ being Element of the carrier of S holds
( not b₁ in the carrier of S or not b₂ in the carrier of S or ||.((LP /. b₁) - (LP /. b₂)).|| <= (K + 1) * ||.(b₁ - b₂).|| ) ) )
A34: 0 + K < 1 + K by XREAL_1:8;

now

let x1, x2 be Point of S; :: thesis: ( x1 in the carrier of S & x2 in the carrier of S implies ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| )
assume that
x1 in the carrier of S and
x2 in the carrier of S ; :: thesis: ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).||
A35: ||.((modetrans (L,S,T)) . (x1 - x2)).|| <= K * ||.(x1 - x2).|| by A33;
0 <= ||.(x1 - x2).|| by NORMSP_1:4;
then A36: K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A34, XREAL_1:64;
||.((LP /. x1) - (LP /. x2)).|| = ||.(((modetrans (L,S,T)) . x1) - (LP /. x2)).|| by A31, PARTFUN1:def 6
.= ||.(((modetrans (L,S,T)) . x1) + (- ((modetrans (L,S,T)) . x2))).|| by A31, PARTFUN1:def 6
.= ||.(((modetrans (L,S,T)) . x1) + ((- 1) * ((modetrans (L,S,T)) . x2))).|| by RLVECT_1:16
.= ||.(((modetrans (L,S,T)) . x1) + ((modetrans (L,S,T)) . ((- 1) * x2))).|| by LOPBAN_1:def 5
.= ||.((modetrans (L,S,T)) . (x1 + ((- 1) * x2))).|| by GRCAT_1:def 8
.= ||.((modetrans (L,S,T)) . (x1 - x2)).|| by RLVECT_1:16 ;
hence ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by A35, A36, XXREAL_0:2; :: thesis: verum

end;

hence ( not K + 1 <= 0 & ( for b₁, b₂ being Element of the carrier of S holds
( not b₁ in the carrier of S or not b₂ in the carrier of S or ||.((LP /. b₁) - (LP /. b₂)).|| <= (K + 1) * ||.(b₁ - b₂).|| ) ) ) by A32; :: thesis: verum

end;

then A37: LP is_continuous_on the carrier of S by NFCONT_1:45;
A38: rng c c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom f )
assume y in rng c ; :: thesis: y in dom f
then y = x0 by A3, TARSKI:def 1;
then y in N by NFCONT_1:4;
hence y in dom f by A2; :: thesis: verum

end;

A39: ( h ^\ n is convergent & rng (h ^\ n) c= the carrier of S ) by Def4;
then A40: LP /* (h ^\ n) is convergent by A37, A19, NFCONT_1:18;
A41: R /* (h ^\ n) is convergent by Th27;
then A42: (LP /* (h ^\ n)) + (R /* (h ^\ n)) is convergent by A40, NORMSP_1:19;
LP /. (0. S) = (modetrans (L,S,T)) . (0. S) by A31, PARTFUN1:def 6
.= (modetrans (L,S,T)) . (0 * (0. S)) by RLVECT_1:10
.= 0 * ((modetrans (L,S,T)) . (0. S)) by LOPBAN_1:def 5
.= 0. T by RLVECT_1:10 ;
then lim (LP /* (h ^\ n)) = 0. T by A37, A39, A19, NFCONT_1:18;
then lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = (0. T) + (0. T) by A41, A23, A40, NORMSP_1:25;
then A43: lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = 0. T by RLVECT_1:4;
rng (h + c) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in dom f )
assume y in rng (h + c) ; :: thesis: y in dom f
then y in N by A4;
hence y in dom f by A2; :: thesis: verum

end;

then (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = ((f /* (h + c)) ^\ n) - (f /* (c ^\ n)) by VALUED_0:27
.= ((f /* (h + c)) ^\ n) - ((f /* c) ^\ n) by A38, VALUED_0:27
.= ((f /* (h + c)) - (f /* c)) ^\ n by Th16 ;
hence ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) by A30, A42, A43, LOPBAN_3:10, LOPBAN_3:11; :: thesis: verum