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;
(Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then rng (Sgm ((Seg (len p)) \ (p " A))) c= dom p by A1, FINSEQ_1:def 13;
then A2: dom (Sgm ((Seg (len p)) \ (p " A))) = dom (p - A) by A1, RELAT_1:27;
A3: dom (Sgm ((Seg (len p)) \ (p " A))) = Seg (len (Sgm ((Seg (len p)) \ (p " A)))) by FINSEQ_1:def 3;
A4: p " A c= Seg (len p)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p " A or x in Seg (len p) )
A5: p " A c= dom p by RELAT_1:132;
A6: dom p = Seg (len p) by FINSEQ_1:def 3;
assume x in p " A ; :: thesis: x in Seg (len p)
hence x in Seg (len p) by A5, A6; :: thesis: verum
end;
len (Sgm ((Seg (len p)) \ (p " A))) = card ((Seg (len p)) \ (p " A)) by Th37, XBOOLE_1:36;
then len (p - A) = card ((Seg (len p)) \ (p " A)) by A2, A3, FINSEQ_1:def 3;
hence len (p - A) = (card (Seg (len p))) - (card (p " A)) by A4, CARD_2:44
.= (len p) - (card (p " A)) by FINSEQ_1:57 ;
:: thesis: verum