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
A1: dom (p - A) = Seg (len (p - A)) by FINSEQ_1:def 3;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
len (p - A) <= len p by Th58;
hence dom (p - A) c= dom p by A1, A2, FINSEQ_1:5; :: thesis: verum