let i be natural number ; :: thesis: for p being FinSequence holds
( ( i in dom p implies ex m being Nat st
( len p = m + 1 & len (Del p,i) = m ) ) & ( not i in dom p implies Del p,i = p ) )
let p be FinSequence; :: thesis: ( ( i in dom p implies ex m being Nat st
( len p = m + 1 & len (Del p,i) = m ) ) & ( not i in dom p implies Del p,i = p ) )

hereby :: thesis: ( not i in dom p implies Del p,i = p )

not i in (Seg (len p)) \ {i}

proof

assume i in (Seg (len p)) \ {i} ; :: thesis: contradiction
then not i in {i} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then A1: card (((Seg (len p)) \ {i}) \/ {i}) = (card ((Seg (len p)) \ {i})) + 1 by CARD_2:54;
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:12;
reconsider r = p as Function of D9,D by FUNCT_2:3;
A3: dom p = Seg (len p) by FINSEQ_1:def 3;
for x being set 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) by TARSKI:def 3;
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:37;
i in Seg (len p) by A2, FINSEQ_1:def 3;
then for x being set st x in {i} holds
x in Seg (len p) by TARSKI:def 1;
then {i} c= Seg (len p) by TARSKI:def 3;
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:78;
then len (Sgm ((Seg (len p)) \ {i})) = m by A4, Th44;
hence ( len p = m + 1 & len (Del p,i) = m ) by A5, A6, FINSEQ_1:def 3; :: thesis: verum

end;

assume not i in dom p ; :: thesis: Del p,i = p
then for x being set st x in {i} holds
not x in dom p by TARSKI:def 1;
then {i} misses dom p by XBOOLE_0:3;
hence Del p,i = p * (Sgm (dom p)) by XBOOLE_1:83
.= p * (Sgm (Seg (len p))) by FINSEQ_1:def 3
.= p * (idseq (len p)) by Th54
.= p | (Seg (len p)) by RELAT_1:94
.= p | (dom p) by FINSEQ_1:def 3
.= p by RELAT_1:97 ;
:: thesis: verum