take
0Functional V
; :: thesis: ( 0Functional V is additive & 0Functional V is cmplxhomogeneous & 0Functional V is 0-preserving )

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

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