let n be Element of NAT ; :: thesis: #Z n is_differentiable_on REAL
A1: dom (#Z n) = REAL by FUNCT_2:def 1;
for x being Real st x in REAL holds
(#Z n) | REAL is_differentiable_in x
proof
let x be Real; :: thesis: ( x in REAL implies (#Z n) | REAL is_differentiable_in x )
assume x in REAL ; :: thesis: (#Z n) | REAL is_differentiable_in x
#Z n is_differentiable_in x by TAYLOR_1:2;
hence (#Z n) | REAL is_differentiable_in x by A1, RELAT_1:68; :: thesis: verum
end;
hence #Z n is_differentiable_on REAL by A1, FDIFF_1:def 6; :: thesis: verum