let F be RealNormSpace; :: thesis: ex R being RestFunc of F st
( R /. 0 = 0. F & R is_continuous_in 0 )
( ([#] REAL) ` = {} REAL & REAL c= REAL & [#] REAL = REAL ) by XBOOLE_1:37;
then reconsider Z = [#] REAL as open Subset of REAL by Lm1, RCOMP_1:def 5;
set R = REAL --> (0. F);
reconsider f = REAL --> (0. F) as PartFunc of REAL, the carrier of F ;
A1: dom (REAL --> (0. F)) = REAL ;
now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )
now :: thesis: for n being Nat holds ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
let n be Nat; :: thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) ;
A3: n in NAT by ORDINAL1:def 12;
thus ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def 2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by RLVECT_1:10 ; :: thesis: verum
end;
then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def 18;
hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; :: thesis: verum
end;
then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
set L = REAL --> (0. F);
now :: thesis: for p being Real holds (REAL --> (0. F)) /. p = p * (0. F)
let p be Real; :: thesis: (REAL --> (0. F)) /. p = p * (0. F)
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (REAL --> (0. F)) /. p = (REAL --> (0. F)) /. pp
.= 0. F
.= p * (0. F) by RLVECT_1:10 ; :: thesis: verum
end;
then reconsider L = REAL --> (0. F) as LinearFunc of F by Def2;
A5: f | Z is constant ;
consider r being Point of F such that
A6: for x being Element of REAL st x in Z /\ (dom f) holds
f . x = r by A5, PARTFUN2:57;
A7: now :: thesis: for x being Real st x in Z /\ (dom f) holds
f /. x = r
let x be Real; :: thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A8: x in Z /\ (dom f) ; :: thesis: f /. x = r
then x in dom f ;
hence f /. x = f . x by PARTFUN1:def 6
.= r by A8, A6 ;
:: thesis: verum
end;
A9: now :: thesis: for x0 being Real st x0 in Z holds
f is_differentiable_in x0
let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A10: x0 in Z ; :: thesis: f is_differentiable_in x0
set N = the Neighbourhood of x0;
for x being Real st x in the Neighbourhood of x0 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
A12: x0 in Z /\ (dom f) by A10;
let x be Real; :: thesis: ( x in the Neighbourhood of x0 implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A13: x - x0 in REAL by XREAL_0:def 1;
then A14: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7, A13 ;
assume x in the Neighbourhood of x0 ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) ;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A12
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7, A13
.= L /. (x - x0) by A1, PARTFUN1:def 6, A13
.= (L /. (x - x0)) + (R /. (x - x0)) by A14, RLVECT_1:4 ;
:: thesis: verum
end;
hence f is_differentiable_in x0 ; :: thesis: verum
end;
set x0 = the Element of REAL ;
f is_differentiable_in the Element of REAL by A9;
then consider N being Neighbourhood of the Element of REAL such that
N c= dom f and
A15: ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. the Element of REAL ) = (L /. (x - the Element of REAL )) + (R /. (x - the Element of REAL )) ;
consider L being LinearFunc of F, R being RestFunc of F such that
A16: for x being Real st x in N holds
(f /. x) - (f /. the Element of REAL ) = (L /. (x - the Element of REAL )) + (R /. (x - the Element of REAL )) by A15;
take R ; :: thesis: ( R /. 0 = 0. F & R is_continuous_in 0 )
consider p being Point of F such that
A17: for r being Real holds L /. r = r * p by Def2;
(f /. the Element of REAL ) - (f /. the Element of REAL ) = (L /. ( the Element of REAL - the Element of REAL )) + (R /. ( the Element of REAL - the Element of REAL )) by A16, RCOMP_1:16;
then 0. F = (L /. ( the Element of REAL - the Element of REAL )) + (R /. ( the Element of REAL - the Element of REAL )) by RLVECT_1:15;
then 0. F = (0 * p) + (R /. 0) by A17;
then 0. F = (0. F) + (R /. 0) by RLVECT_1:10;
hence A18: R /. 0 = 0. F by RLVECT_1:4; :: thesis: R is_continuous_in 0
A19: now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( R /* h is convergent & lim (R /* h) = R /. 0 )
set s3 = seq_const 0;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R /. 0 )
A20: (seq_const 0) . 1 = 0 ;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F ) by Def1;
then ||.((h ") (#) (R /* h)).|| is bounded by LOPBAN_1:20, SEQ_2:13;
then consider M being Real such that
M > 0 and
A21: for n being Nat holds |.(||.((h ") (#) (R /* h)).|| . n).| < M by SEQ_2:3;
A22: now :: thesis: for n being Element of NAT holds ||.(((h ") (#) (R /* h)) . n).|| < M
let n be Element of NAT ; :: thesis: ||.(((h ") (#) (R /* h)) . n).|| < M
|.(||.((h ") (#) (R /* h)).|| . n).| < M by A21;
then |.||.(((h ") (#) (R /* h)) . n).||.| < M by NORMSP_0:def 4;
hence ||.(((h ") (#) (R /* h)) . n).|| < M by ABSVALUE:def 1; :: thesis: verum
end;
reconsider z0 = 0 as Real ;
A23: now :: thesis: for n being Element of NAT holds ||.((R /* h) . n).|| <= (M (#) (abs h)) . n
let n be Element of NAT ; :: thesis: ||.((R /* h) . n).|| <= (M (#) (abs h)) . n
||.(((h ") (#) (R /* h)) . n).|| = ||.(((h ") . n) * ((R /* h) . n)).|| by NDIFF_1:def 2
.= ||.(((h . n) ") * ((R /* h) . n)).|| by VALUED_1:10 ;
then A24: ||.(((h . n) ") * ((R /* h) . n)).|| <= M by A22;
|.(h . n).| >= 0 by COMPLEX1:46;
then |.(h . n).| * ||.(((h . n) ") * ((R /* h) . n)).|| <= M * |.(h . n).| by A24, XREAL_1:64;
then ||.((h . n) * (((h . n) ") * ((R /* h) . n))).|| <= M * |.(h . n).| by NORMSP_1:def 1;
then A25: ||.(((h . n) * ((h . n) ")) * ((R /* h) . n)).|| <= M * |.(h . n).| by RLVECT_1:def 7;
h . n <> 0 by SEQ_1:5;
then ||.(1 * ((R /* h) . n)).|| <= M * |.(h . n).| by A25, XCMPLX_0:def 7;
then ||.((R /* h) . n).|| <= M * |.(h . n).| by RLVECT_1:def 8;
then ||.((R /* h) . n).|| <= M * ((abs h) . n) by SEQ_1:12;
hence ||.((R /* h) . n).|| <= (M (#) (abs h)) . n by SEQ_1:9; :: thesis: verum
end;
lim h = z0 ;
then lim (abs h) = |.z0.| by SEQ_4:14
.= z0 by ABSVALUE:2 ;
then A26: lim (M (#) (abs h)) = M * z0 by SEQ_2:8
.= lim (seq_const 0) by A20, SEQ_4:25 ;
reconsider z0 = 0 as Real ;
lim (M (#) (abs h)) = 0 by A26, A20, SEQ_4:25;
hence ( R /* h is convergent & lim (R /* h) = R /. 0 ) by A18, A23, Th1; :: thesis: verum
end;
R is total by Def1;
then A27: dom R = REAL by FUNCT_2:def 1;
now :: thesis: for s1 being Real_Sequence st rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Nat holds s1 . n <> 0 ) holds
( R /* s1 is convergent & R /. (In (0,REAL)) = lim (R /* s1) )
let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Nat holds s1 . n <> 0 ) implies ( R /* s1 is convergent & R /. (In (0,REAL)) = lim (R /* s1) ) )
assume that
rng s1 c= dom R and
A28: ( s1 is convergent & lim s1 = 0 ) and
A29: for n being Nat holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & R /. (In (0,REAL)) = lim (R /* s1) )
for n being Nat holds s1 . n <> 0 by A29;
then s1 is non-zero by SEQ_1:5;
then s1 is non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def 1;
hence ( R /* s1 is convergent & R /. (In (0,REAL)) = lim (R /* s1) ) by A19; :: thesis: verum
end;
hence R is_continuous_in 0 by A27, NFCONT_3:7; :: thesis: verum