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 )
A1: dom (p - A) = Seg (len (p - A)) by FINSEQ_1:def 3;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
assume dom (p - A) = dom p ; :: thesis: A misses rng p
hence A misses rng p by A1, A2, Th59, FINSEQ_1:6; :: thesis: verum