take 0Functional V ; :: thesis: 0Functional V is constant
thus 0Functional V is constant ; :: thesis: verum