theorem Th81: :: FINSEQ_3:83

for p, q being FinSequence
for A being set
for k being Nat st len p = k + 1 & q = p | (Seg k) holds
( p . (k + 1) in A iff p - A = q - A )