:: deftheorem defines RLSp_PFunct LPSPACE1:def 7 :
for A being non empty set holds RLSp_PFunct A = RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);