:: deftheorem defines [: VECTSP12:def 7 :
for K being Ring
for G, F being non empty ModuleStr over K holds [:G,F:] = ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #);