let p be FinSequence; :: thesis: for D, A being set st p is FinSequence of D holds
p - A is FinSequence of D
let D, A 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 ( rng p c= D & rng (p - A) = (rng p) \ A & (rng p) \ A c= rng p ) by Th72, FINSEQ_1:def 4;
then rng (p - A) c= D by XBOOLE_1:1;
hence p - A is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum