take f = the carrier of R --> (0. R); :: thesis: f is derivation
thus f is derivation ; :: thesis: verum