take REAL --> (0* n) ; :: thesis: REAL --> (0* n) is differentiable
thus REAL --> (0* n) is differentiable ; :: thesis: verum