theorem :: FINSEQ_3:72

for p being FinSequence holds p - (rng p) = {} by Th66;