let X be set ; for f being PartFunc of REAL,REAL
for x being Real st x in X & f | X is_differentiable_in x holds
f is_differentiable_in x
let f be PartFunc of REAL,REAL; for x being Real st x in X & f | X is_differentiable_in x holds
f is_differentiable_in x
let x be Real; ( x in X & f | X is_differentiable_in x implies f is_differentiable_in x )
assume that
A1:
x in X
and
A2:
f | X is_differentiable_in x
; f is_differentiable_in x
consider N being Neighbourhood of x such that
A3:
N c= dom (f | X)
and
A4:
ex L being LinearFunc ex R being RestFunc st
for x1 being Real st x1 in N holds
((f | X) . x1) - ((f | X) . x) = (L . (x1 - x)) + (R . (x1 - x))
by A2;
A5:
(f | X) . x = f . x
by A1, FUNCT_1:49;
take
N
; FDIFF_1:def 4 ( N c= dom f & ex b1 being Element of K16(K17(REAL,REAL)) ex b2 being Element of K16(K17(REAL,REAL)) st
for b3 being object holds
( not b3 in N or (f . b3) - (f . x) = (b1 . (b3 - x)) + (b2 . (b3 - x)) ) )
N c= (dom f) /\ X
by A3, RELAT_1:61;
hence
N c= dom f
by XBOOLE_1:18; ex b1 being Element of K16(K17(REAL,REAL)) ex b2 being Element of K16(K17(REAL,REAL)) st
for b3 being object holds
( not b3 in N or (f . b3) - (f . x) = (b1 . (b3 - x)) + (b2 . (b3 - x)) )
consider L being LinearFunc, R being RestFunc such that
A6:
for x1 being Real st x1 in N holds
((f | X) . x1) - ((f | X) . x) = (L . (x1 - x)) + (R . (x1 - x))
by A4;
take
L
; ex b1 being Element of K16(K17(REAL,REAL)) st
for b2 being object holds
( not b2 in N or (f . b2) - (f . x) = (L . (b2 - x)) + (b1 . (b2 - x)) )
take
R
; for b1 being object holds
( not b1 in N or (f . b1) - (f . x) = (L . (b1 - x)) + (R . (b1 - x)) )
let x1 be Real; ( not x1 in N or (f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x)) )
assume A7:
x1 in N
; (f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x))
then
(f | X) . x1 = f . x1
by A3, FUNCT_1:47;
hence
(f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x))
by A6, A7, A5; verum