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 )

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))

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

then A31: rng (h ^\ n) c= dom (modetrans (L,S,T)) ;

A33: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def 1;

LP is_Lipschitzian_on the carrier of S

A40: rng c c= dom f

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

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

then consider n being Element of NAT such that
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 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

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

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;
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;((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

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

A30:
dom (modetrans (L,S,T)) = the carrier of S
by FUNCT_2:def 1;
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;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

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

then A32:
(f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n))
by FUNCT_2:63;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;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

A33: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def 1;

LP is_Lipschitzian_on the carrier of S

proof

then A39:
LP is_continuous_on the carrier of S
by NFCONT_1:45;
thus
the carrier of S c= dom LP
by FUNCT_2:def 1; :: according to NFCONT_1:def 9 :: thesis: ex b_{1} being object st

( not b_{1} <= 0 & ( for b_{2}, b_{3} being Element of the carrier of S holds

( not b_{2} in the carrier of S or not b_{3} in the carrier of S or ||.((LP /. b_{2}) - (LP /. b_{3})).|| <= b_{1} * ||.(b_{2} - b_{3}).|| ) ) )

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_{1}, b_{2} being Element of the carrier of S holds

( not b_{1} in the carrier of S or not b_{2} in the carrier of S or ||.((LP /. b_{1}) - (LP /. b_{2})).|| <= (K + 1) * ||.(b_{1} - b_{2}).|| ) ) )

A36: 0 + K < 1 + K by XREAL_1:8;

_{1}, b_{2} being Element of the carrier of S holds

( not b_{1} in the carrier of S or not b_{2} in the carrier of S or ||.((LP /. b_{1}) - (LP /. b_{2})).|| <= (K + 1) * ||.(b_{1} - b_{2}).|| ) ) )
by A34; :: thesis: verum

end;( not b

( not 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

( not 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).||

hence
( not K + 1 <= 0 & ( for b||.((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;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

( not b

A40: rng c c= dom f

proof

A41:
( h ^\ n is convergent & rng (h ^\ n) c= the carrier of S )
by Def4;
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;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

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