theorem Th57: :: FINSEQ_3:59

for p being FinSequence
for A being set holds len (p - A) = (len p) - (card (p " A))