take 0RFunctional V ; :: thesis: ( 0RFunctional V is additive & 0RFunctional V is Real_homogeneous & 0RFunctional V is homogeneous )
thus ( 0RFunctional V is additive & 0RFunctional V is Real_homogeneous & 0RFunctional V is homogeneous ) ; :: thesis: verum