theorem Th82: :: FINSEQ_3:84

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