:: deftheorem defines FuncUnit CLOPBAN2:def 5 :
for X being ComplexNormSpace holds FuncUnit X = id the carrier of X;