let X be set ; :: thesis: 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; :: thesis: for x being Real st x in X & f | X is_differentiable_in x holds
f is_differentiable_in x
let x be Real; :: thesis: ( 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 ; :: thesis: 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 ; :: according to FDIFF_1:def 4 :: thesis: ( N c= dom f & ex b₁ being Element of K16(K17(REAL,REAL)) ex b₂ being Element of K16(K17(REAL,REAL)) st
for b₃ being object holds
( not b₃ in N or (f . b₃) - (f . x) = (b₁ . (b₃ - x)) + (b₂ . (b₃ - x)) ) )
N c= (dom f) /\ X by A3, RELAT_1:61;
hence N c= dom f by XBOOLE_1:18; :: thesis: ex b₁ being Element of K16(K17(REAL,REAL)) ex b₂ being Element of K16(K17(REAL,REAL)) st
for b₃ being object holds
( not b₃ in N or (f . b₃) - (f . x) = (b₁ . (b₃ - x)) + (b₂ . (b₃ - 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 ; :: thesis: ex b₁ being Element of K16(K17(REAL,REAL)) st
for b₂ being object holds
( not b₂ in N or (f . b₂) - (f . x) = (L . (b₂ - x)) + (b₁ . (b₂ - x)) )
take R ; :: thesis: for b₁ being object holds
( not b₁ in N or (f . b₁) - (f . x) = (L . (b₁ - x)) + (R . (b₁ - x)) )
let x1 be Real; :: thesis: ( not x1 in N or (f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x)) )
assume A7: x1 in N ; :: thesis: (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; :: thesis: verum