let p be FinSequence; :: thesis: for A being set st dom (p - A) = dom p holds
A misses rng p
let A be set ; :: thesis: ( dom (p - A) = dom p implies A misses rng p )
assume A1: dom (p - A) = dom p ; :: thesis: A misses rng p
( dom (p - A) = Seg (len (p - A)) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
hence A misses rng p by A1, Th68, FINSEQ_1:8; :: thesis: verum