not i in (Seg (len p)) \ {i} then A1: card (((Seg (len p)) \ {i}) \/ {i}) = (card ((Seg (len p)) \ {i})) + 1 by CARD_2:41;
assume A2: i in dom p ; :: thesis: ex m being Nat st
( len p = m + 1 & len (Del (p,i)) = m )
then reconsider D9 = dom p as non empty set ;
reconsider D = rng p as non empty set by A2, FUNCT_1:3;
reconsider r = p as Function of D9,D by FUNCT_2:1;
A3: dom p = Seg (len p) by FINSEQ_1:def 3;
for x being object st x in (Seg (len p)) \ {i} holds
x in Seg (len p) by XBOOLE_0:def 5;
then A4: (Seg (len p)) \ {i} c= Seg (len p) ;
then rng (Sgm ((Seg (len p)) \ {i})) c= Seg (len p) by FINSEQ_1:def 13;
then reconsider q = Sgm ((dom p) \ {i}) as FinSequence of D9 by A3, FINSEQ_1:def 4;
p <> {} by A2;
then consider m being Nat such that
A5: len p = m + 1 by NAT_1:6;
take m = m; :: thesis: ( len p = m + 1 & len (Del (p,i)) = m )
A6: len (r * q) = len q by FINSEQ_2:33;
i in Seg (len p) by A2, FINSEQ_1:def 3;
then for x being object st x in {i} holds
x in Seg (len p) by TARSKI:def 1;
then {i} c= Seg (len p) ;
then card (Seg (len p)) = (card ((Seg (len p)) \ {i})) + 1 by A1, XBOOLE_1:45;
then (card ((Seg (len p)) \ {i})) + 1 = m + 1 by A5, FINSEQ_1:57;
then len (Sgm ((Seg (len p)) \ {i})) = m by A4, Th37;
hence ( len p = m + 1 & len (Del (p,i)) = m ) by A5, A6, FINSEQ_1:def 3; :: thesis: verum