let p be FinSequence; :: thesis: for A being set holds len (p - A) = (len p) - (card (p " A))
let A be set ; :: thesis: len (p - A) = (len p) - (card (p " A))
set q = Sgm ((Seg (len p)) \ (p " A));
A1: Seg (len p) = dom p by FINSEQ_1:def 3;
A2: (Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then ( rng (Sgm ((Seg (len p)) \ (p " A))) c= dom p & p - A = p * (Sgm ((Seg (len p)) \ (p " A))) ) by A1, FINSEQ_1:def 13;
then ( dom (Sgm ((Seg (len p)) \ (p " A))) = dom (p - A) & len (Sgm ((Seg (len p)) \ (p " A))) = card ((Seg (len p)) \ (p " A)) & dom (Sgm ((Seg (len p)) \ (p " A))) = Seg (len (Sgm ((Seg (len p)) \ (p " A)))) ) by A2, Th44, FINSEQ_1:def 3, RELAT_1:46;
then A3: len (p - A) = card ((Seg (len p)) \ (p " A)) by FINSEQ_1:def 3;
p " A c= Seg (len p)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in p " A or x in Seg (len p) )
assume A4: x in p " A ; :: thesis: x in Seg (len p)
( p " A c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:167;
hence x in Seg (len p) by A4; :: thesis: verum

end;

hence len (p - A) = (card (Seg (len p))) - (card (p " A)) by A3, CARD_2:63
.= (len p) - (card (p " A)) by FINSEQ_1:78 ;
:: thesis: verum