let p be FinSequence; :: thesis: for A being set st len (p - A) = len p holds
A misses rng p
let A be set ; :: thesis: ( len (p - A) = len p implies A misses rng p )
assume A1: len (p - A) = len p ; :: thesis: A misses rng p
assume A meets rng p ; :: thesis: contradiction
then p " A <> {} by RELAT_1:173;
then ( not p " A, {} are_equipotent & p " A c= dom p & dom p = Seg (len p) & Seg (len p) is finite ) by CARD_1:46, FINSEQ_1:def 3, RELAT_1:167;
then ( 0 <> card (p " A) & 0 <= card (p " A) ) by CARD_1:21, CARD_1:47;
then ( 0 < card (p " A) & len (p - A) = (len p) - (card (p " A)) ) by Th66;
hence contradiction by A1; :: thesis: verum