let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

f is_continuous_in x0

let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds

f is_continuous_in x0

let x0 be Point of S; :: thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )

assume A1: f is_differentiable_in x0 ; :: thesis: f is_continuous_in x0

then consider N being Neighbourhood of x0 such that

A2: N c= dom f and

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 N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;

hence f is_continuous_in x0 by A2, A3, Th27; :: thesis: verum

for x0 being Point of S st f is_differentiable_in x0 holds

f is_continuous_in x0

let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds

f is_continuous_in x0

let x0 be Point of S; :: thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )

assume A1: f is_differentiable_in x0 ; :: thesis: f is_continuous_in x0

then consider N being Neighbourhood of x0 such that

A2: N c= dom f and

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 N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;

A3: now :: thesis: for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

x0 in N
by NFCONT_1:4;( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

consider g being Real such that

A4: 0 < g and

A5: { y where y is Point of S : ||.(y - x0).|| < g } c= N by NFCONT_1:def 1;

reconsider s2 = NAT --> x0 as sequence of S ;

let s1 be sequence of S; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )

assume that

A6: rng s1 c= dom f and

A7: s1 is convergent and

A8: lim s1 = x0 and

A9: for n being Nat holds s1 . n <> x0 ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

consider l being Nat such that

A10: for m being Nat st l <= m holds

||.((s1 . m) - x0).|| < g by A7, A8, A4, NORMSP_1:def 7;

deffunc H_{1}( Nat) -> Element of the carrier of S = (s1 . $1) - (s2 . $1);

consider s3 being sequence of S such that

A11: for n being Element of NAT holds s3 . n = H_{1}(n)
from FUNCT_2:sch 4();

A12: for n being Nat holds s3 . n = H_{1}(n)

reconsider c = s2 ^\ l as constant sequence of S ;

A18: s3 = s1 - s2 by A12, NORMSP_1:def 3;

A19: s2 is convergent by Th18;

then A20: s3 is convergent by A7, A18, NORMSP_1:20;

then A21: s3 ^\ l is convergent by LOPBAN_3:9;

lim s2 = s2 . 0 by Th18

.= x0 ;

then lim s3 = x0 - x0 by A7, A8, A19, A18, NORMSP_1:26

.= 0. S by RLVECT_1:15 ;

then lim (s3 ^\ l) = 0. S by A20, LOPBAN_3:9;

then reconsider h = s3 ^\ l as 0. S -convergent sequence of S by A21, Def4;

.= (f /* s1) ^\ l by A6, VALUED_0:27 ;

A24: rng c = {x0}

A34: rng (h + c) c= N

then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A33, NORMSP_1:19;

hence f /* s1 is convergent by A23, LOPBAN_3:10; :: thesis: f /. x0 = lim (f /* s1)

A38: lim ((f /* (h + c)) - (f /* c)) = 0. T by A17, A1, A2, A24, A34, Th34;

lim (f /* c) = f /. x0 by A29, A33, NORMSP_1:def 7;

then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. T) + (f /. x0) by A37, A38, A33, NORMSP_1:25

.= f /. x0 by RLVECT_1:4 ;

hence f /. x0 = lim (f /* s1) by A37, A33, A23, LOPBAN_3:11, NORMSP_1:19; :: thesis: verum

end;A4: 0 < g and

A5: { y where y is Point of S : ||.(y - x0).|| < g } c= N by NFCONT_1:def 1;

reconsider s2 = NAT --> x0 as sequence of S ;

let s1 be sequence of S; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )

assume that

A6: rng s1 c= dom f and

A7: s1 is convergent and

A8: lim s1 = x0 and

A9: for n being Nat holds s1 . n <> x0 ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

consider l being Nat such that

A10: for m being Nat st l <= m holds

||.((s1 . m) - x0).|| < g by A7, A8, A4, NORMSP_1:def 7;

deffunc H

consider s3 being sequence of S such that

A11: for n being Element of NAT holds s3 . n = H

A12: for n being Nat holds s3 . n = H

proof

let n be Nat; :: thesis: s3 . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

hence s3 . n = H_{1}(n)
by A11; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence s3 . n = H

A13: now :: thesis: for n being Element of NAT holds not s3 . n = 0. S

given n being Element of NAT such that A14:
s3 . n = 0. S
; :: thesis: contradiction

(s1 . n) - (s2 . n) = 0. S by A12, A14;

then (s1 . n) - x0 = 0. S ;

hence contradiction by A9, RLVECT_1:21; :: thesis: verum

end;(s1 . n) - (s2 . n) = 0. S by A12, A14;

then (s1 . n) - x0 = 0. S ;

hence contradiction by A9, RLVECT_1:21; :: thesis: verum

now :: thesis: for n being Nat holds not (s3 ^\ l) . n = 0. S

then A17:
s3 ^\ l is non-zero
by Th7;given n being Nat such that A15:
(s3 ^\ l) . n = 0. S
; :: thesis: contradiction

A16: n + l in NAT by ORDINAL1:def 12;

s3 . (n + l) = 0. S by A15, NAT_1:def 3;

hence contradiction by A13, A16; :: thesis: verum

end;A16: n + l in NAT by ORDINAL1:def 12;

s3 . (n + l) = 0. S by A15, NAT_1:def 3;

hence contradiction by A13, A16; :: thesis: verum

reconsider c = s2 ^\ l as constant sequence of S ;

A18: s3 = s1 - s2 by A12, NORMSP_1:def 3;

A19: s2 is convergent by Th18;

then A20: s3 is convergent by A7, A18, NORMSP_1:20;

then A21: s3 ^\ l is convergent by LOPBAN_3:9;

lim s2 = s2 . 0 by Th18

.= x0 ;

then lim s3 = x0 - x0 by A7, A8, A19, A18, NORMSP_1:26

.= 0. S by RLVECT_1:15 ;

then lim (s3 ^\ l) = 0. S by A20, LOPBAN_3:9;

then reconsider h = s3 ^\ l as 0. S -convergent sequence of S by A21, Def4;

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

then A22:
((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c)
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n

thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def 2

.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def 3

.= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29

.= ((f /* (h + c)) . n) - (0. T) by RLVECT_1:15

.= (f /* (h + c)) . n by RLVECT_1:13 ; :: thesis: verum

end;thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def 2

.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def 3

.= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29

.= ((f /* (h + c)) . n) - (0. T) by RLVECT_1:15

.= (f /* (h + c)) . n by RLVECT_1:13 ; :: thesis: verum

now :: thesis: for n being Element of NAT holds (h + c) . n = (s1 ^\ l) . n

then A23: ((f /* (h + c)) - (f /* c)) + (f /* c) =
f /* (s1 ^\ l)
by A22, FUNCT_2:63
let n be Element of NAT ; :: thesis: (h + c) . n = (s1 ^\ l) . n

thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A18, Th15

.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3

.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def 2

.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def 3

.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29

.= (s1 . (n + l)) - (0. S) by RLVECT_1:15

.= s1 . (l + n) by RLVECT_1:13

.= (s1 ^\ l) . n by NAT_1:def 3 ; :: thesis: verum

end;thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A18, Th15

.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3

.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def 2

.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def 3

.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29

.= (s1 . (n + l)) - (0. S) by RLVECT_1:15

.= s1 . (l + n) by RLVECT_1:13

.= (s1 ^\ l) . n by NAT_1:def 3 ; :: thesis: verum

.= (f /* s1) ^\ l by A6, VALUED_0:27 ;

A24: rng c = {x0}

proof

thus
rng c c= {x0}
:: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng c

assume y in {x0} ; :: thesis: y in rng c

then A27: y = x0 by TARSKI:def 1;

A28: 0 + l in NAT by ORDINAL1:def 12;

c . 0 = s2 . (0 + l) by NAT_1:def 3

.= y by A27, FUNCOP_1:7, A28 ;

hence y in rng c by NFCONT_1:6; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x0} or y in rng c )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in {x0} )

assume y in rng c ; :: thesis: y in {x0}

then consider n being Nat such that

A25: y = (s2 ^\ l) . n by NFCONT_1:6;

A26: n + l in NAT by ORDINAL1:def 12;

y = s2 . (n + l) by A25, NAT_1:def 3;

then y = x0 by FUNCOP_1:7, A26;

hence y in {x0} by TARSKI:def 1; :: thesis: verum

end;assume y in rng c ; :: thesis: y in {x0}

then consider n being Nat such that

A25: y = (s2 ^\ l) . n by NFCONT_1:6;

A26: n + l in NAT by ORDINAL1:def 12;

y = s2 . (n + l) by A25, NAT_1:def 3;

then y = x0 by FUNCOP_1:7, A26;

hence y in {x0} by TARSKI:def 1; :: thesis: verum

assume y in {x0} ; :: thesis: y in rng c

then A27: y = x0 by TARSKI:def 1;

A28: 0 + l in NAT by ORDINAL1:def 12;

c . 0 = s2 . (0 + l) by NAT_1:def 3

.= y by A27, FUNCOP_1:7, A28 ;

hence y in rng c by NFCONT_1:6; :: thesis: verum

A29: now :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p

then A33:
f /* c is convergent
;ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p )

assume A30: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p )

assume n <= m ; :: thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p

A31: m in NAT by ORDINAL1:def 12;

A32: m + l in NAT by ORDINAL1:def 12;

x0 in N by NFCONT_1:4;

then rng c c= dom f by A2, A24, ZFMISC_1:31;

then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109, A31

.= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def 3

.= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7, A32

.= ||.(0. T).|| by RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A30; :: thesis: verum

end;for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p )

assume A30: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

||.(((f /* c) . m) - (f /. x0)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p )

assume n <= m ; :: thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p

A31: m in NAT by ORDINAL1:def 12;

A32: m + l in NAT by ORDINAL1:def 12;

x0 in N by NFCONT_1:4;

then rng c c= dom f by A2, A24, ZFMISC_1:31;

then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109, A31

.= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def 3

.= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7, A32

.= ||.(0. T).|| by RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A30; :: thesis: verum

A34: rng (h + c) c= N

proof

then A37:
(f /* (h + c)) - (f /* c) is convergent
by A17, A1, A2, A24, Th34;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in N )

assume A35: y in rng (h + c) ; :: thesis: y in N

then consider n being Nat such that

A36: y = (h + c) . n by NFCONT_1:6;

reconsider y1 = y as Point of S by A35;

(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A18, Th15

.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3

.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def 2

.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def 3

.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29

.= (s1 . (n + l)) - (0. S) by RLVECT_1:15

.= s1 . (l + n) by RLVECT_1:13 ;

then ||.(((h + c) . n) - x0).|| < g by A10, NAT_1:12;

then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A36;

hence y in N by A5; :: thesis: verum

end;assume A35: y in rng (h + c) ; :: thesis: y in N

then consider n being Nat such that

A36: y = (h + c) . n by NFCONT_1:6;

reconsider y1 = y as Point of S by A35;

(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A18, Th15

.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3

.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def 2

.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def 3

.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29

.= (s1 . (n + l)) - (0. S) by RLVECT_1:15

.= s1 . (l + n) by RLVECT_1:13 ;

then ||.(((h + c) . n) - x0).|| < g by A10, NAT_1:12;

then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A36;

hence y in N by A5; :: thesis: verum

then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A33, NORMSP_1:19;

hence f /* s1 is convergent by A23, LOPBAN_3:10; :: thesis: f /. x0 = lim (f /* s1)

A38: lim ((f /* (h + c)) - (f /* c)) = 0. T by A17, A1, A2, A24, A34, Th34;

lim (f /* c) = f /. x0 by A29, A33, NORMSP_1:def 7;

then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. T) + (f /. x0) by A37, A38, A33, NORMSP_1:25

.= f /. x0 by RLVECT_1:4 ;

hence f /. x0 = lim (f /* s1) by A37, A33, A23, LOPBAN_3:11, NORMSP_1:19; :: thesis: verum

hence f is_continuous_in x0 by A2, A3, Th27; :: thesis: verum