:: deftheorem defines FS2XFS* AFINSQ_1:def 10 :
for D being non empty set
for q being FinSequence of D
for n being Nat st n > len q & NAT c= D holds
for b₄ being non empty XFinSequence of D holds
( b₄ = FS2XFS* (q,n) iff ( len q = b₄ . 0 & len b₄ = n & ( for i being Nat st 1 <= i & i <= len q holds
b₄ . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b₄ . j = 0 ) ) );