:: deftheorem Def10 defines carr PRVECT_1:def 11 :
for g being non empty 1-sorted-yielding non-Empty FinSequence
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) ) ) );