:: deftheorem Def13 defines zeros PRVECT_1:def 13 :
for g being Group-Sequence
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) );