for A being non empty set holds CPFuncZero A is_a_unity_wrt addcpfunc A