reconsider Z = REAL as open Subset of REAL by Lm2;
reconsider f = REAL --> (0. F) as Function of REAL, the carrier of F ;
take f ; :: thesis: f is differentiable
A1: Z = dom f ;
now :: thesis: for x being Real st x in Z holds
f /. x = (x * (0. F)) + (0. F)
let x be Real; :: thesis: ( x in Z implies f /. x = (x * (0. F)) + (0. F) )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
assume x in Z ; :: thesis: f /. x = (x * (0. F)) + (0. F)
thus f /. x = f /. xx
.= 0. F
.= x * (0. F) by RLVECT_1:10
.= (x * (0. F)) + (0. F) by RLVECT_1:4 ; :: thesis: verum
end;
then f is_differentiable_on Z by A1, Th21;
hence f is differentiable ; :: thesis: verum