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 () by REAL_NS1:def 4;
A3: ( the carrier of () = REAL m & the carrier of () = REAL 1 ) by REAL_NS1:def 4;
then reconsider g = <>* f as PartFunc of (),() ;
reconsider x1 = x as Point of () by REAL_NS1:def 4;
set ZR = 0. ();
A4: 0. () = 0* 1 by REAL_NS1:def 4
.= 1 |-> 0 by EUCLID:def 4
.= by FINSEQ_2:59 ;
A5: 0. () = (REAL m) --> by ;
reconsider Z = X as Subset of () by REAL_NS1:def 4;
A6: Z is open by ;
A7: dom f = X by ;
then A8: dom (<>* f) = X by PDIFF_9:3;
A9: Z = dom g by ;
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 ;
then reconsider x1 = x as Element of REAL m ;
(<>* f) . x = <*(f . x1)*> by ;
hence (<>* f) . x = <*d*> by ; :: thesis: verum
end;
then A11: <>* f = X --> <*d*> by ;
A12: rng g = {rd} by ;
then A13: ( g is_differentiable_on Z & ( for x being Point of () st x in Z holds
(g `| Z) /. x = 0. () ) ) by ;
then A14: g is_differentiable_in x1 by ;
A15: 0. () = (g `| Z) /. x1 by
.= diff (g,x1) by ;
A16: <>* f is_differentiable_in x by ;
hence f is_differentiable_in x by PDIFF_7:def 1; :: thesis: diff (f,x) = (REAL m) --> 0
A17: diff ((<>* f),x) = (REAL m) --> by ;
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
.= (proj (1,1)) . by
.= 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 ; :: thesis: verum