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