([#] V) --> (In (0,REAL)) is RFunctional of V ;
hence ([#] V) --> 0 is RFunctional of V ; :: thesis: verum