let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is_differentiable_on X holds
f is_differentiable_on X
let f be PartFunc of REAL,REAL; :: thesis: ( f | X is_differentiable_on X implies f is_differentiable_on X )
assume A1: f | X is_differentiable_on X ; :: thesis: f is_differentiable_on X

A2: now

let x be Real; :: thesis: ( x in X implies f | X is_differentiable_in x )
assume A3: x in X ; :: thesis: f | X is_differentiable_in x
then (f | X) | X is_differentiable_in x by A1, FDIFF_1:def 6;
hence f | X is_differentiable_in x by A3, Th4; :: thesis: verum

end;

X c= dom (f | X) by A1, FDIFF_1:def 6;
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, FDIFF_1:def 6; :: thesis: verum