let i be Nat; 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; ( ( 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 ( not i in dom p implies Del (p,i) = p )
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
;
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;
rng (Sgm ((Seg (len p)) \ {i})) = (Seg (len p)) \ {i}
by FINSEQ_1:def 14;
then
rng (Sgm ((Seg (len p)) \ {i})) c= Seg (len p)
by XBOOLE_1:36;
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;
( 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 Th37;
hence
(
len p = m + 1 &
len (Del (p,i)) = m )
by A5, A6, FINSEQ_1:def 3;
verum
assume
not i in dom p
; Del (p,i) = p
then
for x being object 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 Th46
.=
p | (Seg (len p))
by RELAT_1:65
.=
p | (dom p)
by FINSEQ_1:def 3
.=
p
;
verum