theorem :: LPSPACC1:8

for A being non empty set holds CPFuncUnit A is_a_unity_wrt multcpfunc A