set f = the carrier of R --> (0. R);
the carrier of R --> (0. R) is derivation ;
then the carrier of R --> (0. R) in Der R ;
hence not Der R is empty ; :: thesis: verum