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