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