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