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;

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;

hence diff (f,x) = (REAL m) --> 0 by PDIFF_7:def 2, A18; :: thesis: verum

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*>

then A11:
<>* f = X --> <*d*>
by A8, FUNCOP_1:11;(<>* 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;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

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

then
(proj (1,1)) * (diff ((<>* f),x)) = (dom ((proj (1,1)) * (diff ((<>* f),x)))) --> 0
by FUNCOP_1:11;((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;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

hence diff (f,x) = (REAL m) --> 0 by PDIFF_7:def 2, A18; :: thesis: verum