:: deftheorem Def13 defines zeros PRVECT_1:def 14 :
for g being non empty non-empty-addLoopStr-yielding FinSequence
for b₂ being Element of product (carr g) holds
( b₂ = zeros g iff for i being Element of dom (carr g) holds b₂ . i = 0. (g . i) );