let m be non zero Element of NAT ; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( x in X implies ( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 ) )
assume A2: x in X ; :: thesis: ( 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;

now :: thesis: for x being object st x in dom (<>* f) holds
(<>* f) . x = <*d*>

let x be object ; :: thesis: ( x in dom (<>* f) implies (<>* f) . x = <*d*> )
assume x in dom (<>* f) ; :: thesis: (<>* f) . x = <*d*>
then A10: x in X by A7, PDIFF_9:3;
then reconsider x1 = x as Element of REAL m ;
(<>* f) . x = <*(f . x1)*> by A7, A10, PDIFF_9:6;
hence (<>* f) . x = <*d*> by A1, A10, FUNCOP_1:7; :: thesis: verum

end;

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; :: thesis: 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 :: thesis: 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 ; :: thesis: ( 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))) ; :: thesis: ((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 ; :: thesis: 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; :: thesis: verum