let X be set ; :: thesis: for f being PartFunc of REAL,REAL holds
( f | X is_differentiable_on X iff f is_differentiable_on X )
let f be PartFunc of REAL,REAL; :: thesis: ( f | X is_differentiable_on X iff f is_differentiable_on X )

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

assume A1: f | X is_differentiable_on X ; :: thesis: f is_differentiable_on X
then A2: for x being Real st x in X holds
f | X is_differentiable_in x ;
X c= dom (f | X) by A1;
then X c= (dom f) /\ X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
hence f is_differentiable_on X by A2; :: thesis: verum

end;

thus ( f is_differentiable_on X implies f | X is_differentiable_on X ) by RELAT_1:62; :: thesis: verum