:: deftheorem defines product PRVECT_1:def 15 :
for G being non empty non-empty-addLoopStr-yielding FinSequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);