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 x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

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 x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let X be non empty Subset of (REAL m); :: thesis: for d being Real st X is open & f = X --> d holds

for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let d be Real; :: thesis: ( X is open & f = X --> d implies for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) )

assume A1: ( X is open & f = X --> d ) ; :: thesis: for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) )

assume A2: ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

take s = 1; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

thus 0 < s ; :: thesis: for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|

let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| )

assume A3: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|

let v be Element of REAL m; :: thesis: |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|

A4: (diff (f,x1)) . v = ((REAL m) --> 0) . v by A1, Th12, A3

.= 0 by FUNCOP_1:7 ;

(diff (f,x0)) . v = ((REAL m) --> 0) . v by A1, Th12, A2

.= 0 by FUNCOP_1:7 ;

hence |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| by A4, A2, COMPLEX1:44; :: thesis: verum

for X being non empty Subset of (REAL m)

for d being Real st X is open & f = X --> d holds

for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

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 x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let X be non empty Subset of (REAL m); :: thesis: for d being Real st X is open & f = X --> d holds

for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let d be Real; :: thesis: ( X is open & f = X --> d implies for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) )

assume A1: ( X is open & f = X --> d ) ; :: thesis: for x0 being Element of REAL m

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) )

assume A2: ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

take s = 1; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )

thus 0 < s ; :: thesis: for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds

for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|

let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| )

assume A3: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|

let v be Element of REAL m; :: thesis: |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|

A4: (diff (f,x1)) . v = ((REAL m) --> 0) . v by A1, Th12, A3

.= 0 by FUNCOP_1:7 ;

(diff (f,x0)) . v = ((REAL m) --> 0) . v by A1, Th12, A2

.= 0 by FUNCOP_1:7 ;

hence |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| by A4, A2, COMPLEX1:44; :: thesis: verum