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