let m be non zero Element of NAT ; for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )
let f be PartFunc of (REAL m),REAL; for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )
let X be non empty Subset of (REAL m); for d being Real st X is open & f = X --> d holds
for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )
let d be Real; ( X is open & f = X --> d implies for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 ) )
assume A1:
( X is open & f = X --> d )
; for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )
let x be Element of REAL m; ( x in X implies ( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 ) )
assume A2:
x in X
; ( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )
d in REAL
by XREAL_0:def 1;
then
<*d*> in 1 -tuples_on REAL
by FINSEQ_2:98;
then
<*d*> in REAL 1
by EUCLID:def 1;
then reconsider rd = <*d*> as Point of (REAL-NS 1) by REAL_NS1:def 4;
A3:
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS 1) = REAL 1 )
by REAL_NS1:def 4;
then reconsider g = <>* f as PartFunc of (REAL-NS m),(REAL-NS 1) ;
reconsider x1 = x as Point of (REAL-NS m) by REAL_NS1:def 4;
set ZR = 0. (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)));
A4: 0. (REAL-NS 1) =
0* 1
by REAL_NS1:def 4
.=
1 |-> 0
by EUCLID:def 4
.=
<*0*>
by FINSEQ_2:59
;
A5:
0. (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) = (REAL m) --> <*0*>
by A4, A3, LOPBAN_1:31;
reconsider Z = X as Subset of (REAL-NS m) by REAL_NS1:def 4;
A6:
Z is open
by PDIFF_9:10, A1;
A7:
dom f = X
by A1, FUNCT_2:def 1;
then A8:
dom (<>* f) = X
by PDIFF_9:3;
A9:
Z = dom g
by A7, PDIFF_9:3;
then A11:
<>* f = X --> <*d*>
by A8, FUNCOP_1:11;
A12:
rng g = {rd}
by A11, FUNCOP_1:8;
then A13:
( g is_differentiable_on Z & ( for x being Point of (REAL-NS m) st x in Z holds
(g `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) ) )
by NDIFF_1:33, A6, A9;
then A14:
g is_differentiable_in x1
by A2, NDIFF_1:31, A6;
A15: 0. (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) =
(g `| Z) /. x1
by A12, A2, NDIFF_1:33, A6, A9
.=
diff (g,x1)
by A2, NDIFF_1:def 9, A13
;
A16:
<>* f is_differentiable_in x
by PDIFF_6:2, A14;
hence
f is_differentiable_in x
by PDIFF_7:def 1; diff (f,x) = (REAL m) --> 0
A17:
diff ((<>* f),x) = (REAL m) --> <*0*>
by A5, A15, A16, PDIFF_6:3;
A18:
dom ((proj (1,1)) * (diff ((<>* f),x))) = REAL m
by FUNCT_2:def 1;
now for y being object st y in dom ((proj (1,1)) * (diff ((<>* f),x))) holds
((proj (1,1)) * (diff ((<>* f),x))) . y = 0 let y be
object ;
( y in dom ((proj (1,1)) * (diff ((<>* f),x))) implies ((proj (1,1)) * (diff ((<>* f),x))) . y = 0 )assume A19:
y in dom ((proj (1,1)) * (diff ((<>* f),x)))
;
((proj (1,1)) * (diff ((<>* f),x))) . y = 0 then reconsider y1 =
y as
Element of
REAL m ;
thus ((proj (1,1)) * (diff ((<>* f),x))) . y =
(proj (1,1)) . ((diff ((<>* f),x)) . y1)
by A19, FUNCT_1:12
.=
(proj (1,1)) . <*0*>
by A17, FUNCOP_1:7
.=
0
by PDIFF_1:1
;
verum end;
then
(proj (1,1)) * (diff ((<>* f),x)) = (dom ((proj (1,1)) * (diff ((<>* f),x)))) --> 0
by FUNCOP_1:11;
hence
diff (f,x) = (REAL m) --> 0
by PDIFF_7:def 2, A18; verum