let f be PartFunc of REAL,REAL; :: thesis: for X being Subset of REAL st X is open & X c= dom f holds
( f is_differentiable_on X iff f | X is_differentiable_on X )
let X be Subset of REAL; :: thesis: ( X is open & X c= dom f implies ( f is_differentiable_on X iff f | X is_differentiable_on X ) )
assume that
AS1: X is open and
AS2: X c= dom f ; :: thesis: ( f is_differentiable_on X iff f | X is_differentiable_on X )

hereby :: thesis: ( f | X is_differentiable_on X implies f is_differentiable_on X )

assume A1: f is_differentiable_on X ; :: thesis: f | X is_differentiable_on X
A3: dom (f | X) = X by RELAT_1:62, AS2;

now :: thesis: for x being Real st x in X holds
f | X is_differentiable_in x

let x be Real; :: thesis: ( x in X implies f | X is_differentiable_in x )
assume A4: x in X ; :: thesis: f | X is_differentiable_in x
then f is_differentiable_in x by A1, AS1, FDIFF_1:9;
hence f | X is_differentiable_in x by LM002, AS1, A4; :: thesis: verum

end;

hence f | X is_differentiable_on X by AS1, A3, FDIFF_1:9; :: thesis: verum

end;

assume A1: f | X is_differentiable_on X ; :: thesis: f is_differentiable_on X

now :: thesis: for x being Real st x in X holds
f is_differentiable_in x

let x be Real; :: thesis: ( x in X implies f is_differentiable_in x )
assume A4: x in X ; :: thesis: f is_differentiable_in x
then f | X is_differentiable_in x by A1, AS1, FDIFF_1:9;
hence f is_differentiable_in x by LM002, AS1, A4; :: thesis: verum

end;

hence f is_differentiable_on X by AS1, AS2, FDIFF_1:9; :: thesis: verum