let S, T be 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 0. S -convergent sequence of S st h is non-zero holds
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 0. S -convergent sequence of S st h is non-zero holds
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 0. S -convergent sequence of S st h is non-zero holds
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 0. S -convergent sequence of S st h is non-zero holds
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 0. S -convergent sequence of S st h is non-zero holds
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 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies 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 A3: h is non-zero ; :: 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
A4: rng c = {x0} and
A5: 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
A6: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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;
consider N2 being Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by Th1;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A9: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
consider g being Real such that
A10: 0 < g and
A11: { y where y is Point of S : ||.(y - x0).|| < g } c= N2 by NFCONT_1:def 1;
A12: 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 A4, TARSKI:def 1;
then A13: lim c = x0 by Th18;
A14: ( c is convergent & h is convergent ) by Def4, Th18;
then A15: h + c is convergent by NORMSP_1:19;
lim h = 0. S by Def4;
then lim (h + c) = (0. S) + x0 by A13, A14, NORMSP_1:25
.= x0 by RLVECT_1:4 ;
then consider n being Nat such that
A16: for m being Nat st n <= m holds
||.(((h + c) . m) - x0).|| < g by A10, A15, NORMSP_1:def 7;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A17: rng (c ^\ n) = {x0} by A4, VALUED_0:26;
thus rng (c ^\ n) c= N2 by A12, A17, TARSKI:def 1; :: thesis: rng ((h + c) ^\ n) c= N2
let y be object ; :: 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 Nat such that
A18: y = ((h + c) ^\ n) . m by NFCONT_1:6;
reconsider y1 = y as Point of S by A18;
n + 0 <= n + m by XREAL_1:7;
then ||.(((h + c) . (n + m)) - x0).|| < g by A16;
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 A18;
hence y in N2 by A11; :: thesis: verum

end;

then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A19: rng ((h + c) ^\ n) c= N2 ;
A20: lim (h ^\ n) = 0. S by Def4;
A21: 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 A22: ((h + c) ^\ n) . k in N2 by A19;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by NFCONT_1:6, VALUED_0:26;
then A23: (c ^\ n) . k = x0 by A4, 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 A9, A8, A22, A23; :: 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 ;
A24: h ^\ n is non-zero by A3, Th17;
then A25: lim (R /* (h ^\ n)) = 0. T by Th24;
A26: rng ((h + c) ^\ n) c= dom f by A19, A7, A2;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 2;
then A27: rng (h ^\ n) c= dom R ;
A28: rng (c ^\ n) c= dom f

proof

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

end;

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

now :: thesis: for k being Element of NAT holds ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k

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 A26, FUNCT_2:109
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A28, FUNCT_2:109
.= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A21
.= ((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 A30, PARTFUN1:def 6
.= ((LP /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by A31, FUNCT_2:109
.= ((LP /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A27, FUNCT_2:109
.= ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def 2 ; :: thesis: verum

end;

then A32: (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
A33: 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 object 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
A34: 0 <= K and
A35: 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₂).|| ) ) )
A36: 0 + K < 1 + K by XREAL_1:8;

now :: thesis: for x1, x2 being Point of S st x1 in the carrier of S & x2 in the carrier of S holds
||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).||

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).||
A37: ||.((modetrans (L,S,T)) . (x1 - x2)).|| <= K * ||.(x1 - x2).|| by A35;
0 <= ||.(x1 - x2).|| by NORMSP_1:4;
then A38: K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A36, XREAL_1:64;
||.((LP /. x1) - (LP /. x2)).|| = ||.(((modetrans (L,S,T)) . x1) - (LP /. x2)).|| by A33, PARTFUN1:def 6
.= ||.(((modetrans (L,S,T)) . x1) + (- ((modetrans (L,S,T)) . x2))).|| by A33, 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 VECTSP_1:def 20
.= ||.((modetrans (L,S,T)) . (x1 - x2)).|| by RLVECT_1:16 ;
hence ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by A37, A38, 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 A34; :: thesis: verum

end;

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

proof

let y be object ; :: 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 A4, TARSKI:def 1;
then y in N by NFCONT_1:4;
hence y in dom f by A2; :: thesis: verum

end;

A41: ( h ^\ n is convergent & rng (h ^\ n) c= the carrier of S ) by Def4;
then A42: LP /* (h ^\ n) is convergent by A39, A20, NFCONT_1:18;
A43: R /* (h ^\ n) is convergent by A24, Th24;
then A44: (LP /* (h ^\ n)) + (R /* (h ^\ n)) is convergent by A42, NORMSP_1:19;
LP /. (0. S) = (modetrans (L,S,T)) . (0. S) by A33, 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 A39, A41, A20, NFCONT_1:18;
then lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = (0. T) + (0. T) by A43, A25, A42, NORMSP_1:25;
then A45: lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = 0. T by RLVECT_1:4;
rng (h + c) c= dom f by A5, A2;
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 A40, 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 A32, A44, A45, LOPBAN_3:10, LOPBAN_3:11; :: thesis: verum