theorem Th9: :: LPSPACC1:9

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