:: deftheorem defines Carrier RLVECT_2:def 4 :
for V being non empty addLoopStr
for L being Element of Funcs ( the carrier of V,REAL) holds Carrier L = { v where v is Element of V : L . v <> 0 } ;