reconsider Z = REAL as open Subset of REAL by Lm2;

reconsider f = id REAL as Function of REAL,REAL ;

take f ; :: thesis: f is differentiable

A1: Z = dom f ;

f is_differentiable_on Z by A1, Th17;

hence f is differentiable ; :: thesis: verum

reconsider f = id REAL as Function of REAL,REAL ;

take f ; :: thesis: f is differentiable

A1: Z = dom f ;

f is_differentiable_on Z by A1, Th17;

hence f is differentiable ; :: thesis: verum