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
A2: len (p - A) = (len p) - (card (p " A)) by Th57;
assume A meets rng p ; :: thesis: contradiction
then p " A <> {} by RELAT_1:138;
hence contradiction by A1, A2; :: thesis: verum