:: deftheorem Def7 defines zeros PRVECT_2:def 7 :
for G being RealLinearSpace-Sequence
for b₂ being Element of product (carr G) holds
( b₂ = zeros G iff for j being Element of dom (carr G) holds b₂ . j = the ZeroF of (G . j) );