take 0RFunctional V ; :: thesis: ( 0RFunctional V is additive & 0RFunctional V is 0-preserving )
thus ( 0RFunctional V is additive & 0RFunctional V is 0-preserving ) ; :: thesis: verum