let p be FinSequence; :: thesis: for A, D being set st p is FinSequence of D holds
p - A is FinSequence of D
let A, D be set ; :: thesis: ( p is FinSequence of D implies p - A is FinSequence of D )
assume p is FinSequence of D ; :: thesis: p - A is FinSequence of D
then A1: rng p c= D by FINSEQ_1:def 4;
rng (p - A) = (rng p) \ A by Th63;
then rng (p - A) c= D by A1;
hence p - A is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum