:: deftheorem defines vector-associative CFUNCDOM:def 9 :
for IT being non empty ComplexAlgebraStr holds
( IT is vector-associative iff for x, y being Element of IT
for a being Complex holds a * (x * y) = (a * x) * y );