:: deftheorem Def9 defines @ BSPACE:def 9 :
for X being non empty set
for s being FinSequence of (bspace X)
for x being Element of X
for b₄ being FinSequence of Z_2 holds
( b₄ = s @ x iff ( len b₄ = len s & ( for j being Nat st 1 <= j & j <= len s holds
b₄ . j = (s . j) @ x ) ) );