:: deftheorem defZMQVSp defines Z_MQ_VectSp ZMODUL04:def 5 :
for V being Z_Module st V is Mult-cancelable holds
Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #);