:: deftheorem defines product PRVECT_1:def 14 :
for G being Group-Sequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);