let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
for x being Real st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )
let Z be Subset of REAL; :: thesis: for x being Real st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )
let x0 be Real; :: thesis: ( Z is open & x0 in Z & Z c= dom f implies ( f | Z is_differentiable_in x0 iff f is_differentiable_in x0 ) )
assume A1: ( Z is open & x0 in Z & Z c= dom f ) ; :: thesis: ( f | Z is_differentiable_in x0 iff f is_differentiable_in x0 )

hereby :: thesis: ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 )

assume A2: f | Z is_differentiable_in x0 ; :: thesis: f is_differentiable_in x0
thus f is_differentiable_in x0 :: thesis: verum

proof

consider N being Neighbourhood of x0 such that
A3: N c= dom (f | Z) and
A4: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A2;
consider L being LinearFunc, R being RestFunc such that
A5: for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
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 . x0) = (b₁ . (b₃ - x0)) + (b₂ . (b₃ - x0)) ) )
dom (f | Z) c= dom f by RELAT_1:60;
hence N c= dom f by A3; :: 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 . x0) = (b₁ . (b₃ - x0)) + (b₂ . (b₃ - x0)) )
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 . x0) = (L . (b₂ - x0)) + (b₁ . (b₂ - x0)) )
take R ; :: thesis: for b₁ being object holds
( not b₁ in N or (f . b₁) - (f . x0) = (L . (b₁ - x0)) + (R . (b₁ - x0)) )
let x be Real; :: thesis: ( not x in N or (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A6: x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
then (f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3, A6, FUNCT_1:47;
hence (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, FUNCT_1:49; :: thesis: verum

end;

end;

assume A7: f is_differentiable_in x0 ; :: thesis: f | Z is_differentiable_in x0
consider N1 being Neighbourhood of x0 such that
A8: N1 c= Z by A1, RCOMP_1:18;
consider N being Neighbourhood of x0 such that
A9: N c= dom f and
A10: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A7;
consider N2 being Neighbourhood of x0 such that
A11: N2 c= N1 and
A12: N2 c= N by RCOMP_1:17;
A13: N2 c= Z by A8, A11;
take N2 ; :: according to FDIFF_1:def 4 :: thesis: ( N2 c= dom (f | Z) & 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 N2 or ((f | Z) . b₃) - ((f | Z) . x0) = (b₁ . (b₃ - x0)) + (b₂ . (b₃ - x0)) ) )
N2 c= dom f by A9, A12;
then N2 c= (dom f) /\ Z by A13, XBOOLE_1:19;
hence N2 c= dom (f | Z) by RELAT_1:61; :: 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 N2 or ((f | Z) . b₃) - ((f | Z) . x0) = (b₁ . (b₃ - x0)) + (b₂ . (b₃ - x0)) )
consider L being LinearFunc, R being RestFunc such that
A15: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A10;
take L ; :: thesis: ex b₁ being Element of K16(K17(REAL,REAL)) st
for b₂ being object holds
( not b₂ in N2 or ((f | Z) . b₂) - ((f | Z) . x0) = (L . (b₂ - x0)) + (b₁ . (b₂ - x0)) )
take R ; :: thesis: for b₁ being object holds
( not b₁ in N2 or ((f | Z) . b₁) - ((f | Z) . x0) = (L . (b₁ - x0)) + (R . (b₁ - x0)) )
let x be Real; :: thesis: ( not x in N2 or ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A16: x in N2 ; :: thesis: ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
then (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A12, A15;
then ((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A8, A11, A16, FUNCT_1:49;
hence ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, FUNCT_1:49; :: thesis: verum