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 )

assume A1: i in dom p ; :: thesis: ex m being Nat st
( len p = m + 1 & len (Del p,i) = m )
then p <> {} ;
then A2: len p <> 0 ;
A3: i in Seg (len p) by A1, FINSEQ_1:def 3;
consider m being Nat such that
A4: len p = m + 1 by A2, NAT_1:6;
A5: (Seg (len p)) \ {i} c= Seg (len p)

proof

for x being set st x in (Seg (len p)) \ {i} holds
x in Seg (len p) by XBOOLE_0:def 5;
hence (Seg (len p)) \ {i} c= Seg (len p) by TARSKI:def 3; :: thesis: verum

end;

then A6: rng (Sgm ((Seg (len p)) \ {i})) c= Seg (len p) by FINSEQ_1:def 13;
reconsider D' = dom p as non empty set by A1;
dom p = Seg (len p) by FINSEQ_1:def 3;
then reconsider q = Sgm ((dom p) \ {i}) as FinSequence of D' by A6, FINSEQ_1:def 4;
reconsider D = rng p as non empty set by A1, FUNCT_1:12;
reconsider r = p as Function of D',D by FUNCT_2:3;
A7: len (r * q) = len q by FINSEQ_2:37;
A8: len (Sgm ((Seg (len p)) \ {i})) = m

proof

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

proof

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

end;

then A9: card (((Seg (len p)) \ {i}) \/ {i}) = (card ((Seg (len p)) \ {i})) + 1 by CARD_2:54;
{i} c= Seg (len p)

proof

for x being set st x in {i} holds
x in Seg (len p) by A3, TARSKI:def 1;
hence {i} c= Seg (len p) by TARSKI:def 3; :: thesis: verum

end;

then card (Seg (len p)) = (card ((Seg (len p)) \ {i})) + 1 by A9, XBOOLE_1:45;
then (card ((Seg (len p)) \ {i})) + 1 = m + 1 by A4, FINSEQ_1:78;
hence len (Sgm ((Seg (len p)) \ {i})) = m by A5, Th44; :: thesis: verum

end;

take m = m; :: thesis: ( len p = m + 1 & len (Del p,i) = m )
thus ( len p = m + 1 & len (Del p,i) = m ) by A4, A7, A8, 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