:: deftheorem defines CPFuncUnit LPSPACC1:def 7 :
for A being set holds CPFuncUnit A = A --> 1r;