:: deftheorem defines RealPFuncZero LPSPACE1:def 5 :
for A being non empty set holds RealPFuncZero A = A --> 0;