:: deftheorem Def4 defines carr PRVECT_2:def 4 :
for G being RealLinearSpace-Sequence
for b₂ being Domain-Sequence holds
( b₂ = carr G iff ( len b₂ = len G & ( for j being Element of dom G holds b₂ . j = the carrier of (G . j) ) ) );