let p be FinSequence; :: thesis: for A being set holds dom (p - A) c= dom p
let A be set ; :: thesis: dom (p - A) c= dom p
( dom (p - A) = Seg (len (p - A)) & dom p = Seg (len p) & len (p - A) <= len p ) by Th67, FINSEQ_1:def 3;
hence dom (p - A) c= dom p by FINSEQ_1:7; :: thesis: verum