let a be Element of NAT ; for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
let fs, fs1, fs2 be FinSequence; for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
let v be set ; ( a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 implies Del (fs,a) = fs1 ^ fs2 )
assume that
A1:
a in dom fs
and
A2:
fs = (fs1 ^ <*v*>) ^ fs2
and
A3:
len fs1 = a - 1
; Del (fs,a) = fs1 ^ fs2
A4:
(len (Del (fs,a))) + 1 = len fs
by A1, WSIERP_1:def 1;
len fs =
(len (fs1 ^ <*v*>)) + (len fs2)
by A2, FINSEQ_1:22
.=
((len fs1) + 1) + (len fs2)
by FINSEQ_2:16
.=
a + (len fs2)
by A3
;
then
len (Del (fs,a)) = (len fs2) + (len fs1)
by A3, A4;
then A5:
len (fs1 ^ fs2) = len (Del (fs,a))
by FINSEQ_1:22;
A6:
len <*v*> = 1
by FINSEQ_1:39;
A7:
fs = fs1 ^ (<*v*> ^ fs2)
by A2, FINSEQ_1:32;
then
len fs = (a - 1) + (len (<*v*> ^ fs2))
by A3, FINSEQ_1:22;
then A8:
len (<*v*> ^ fs2) = (len fs) - (a - 1)
;
now for e being Nat st 1 <= e & e <= len (Del (fs,a)) holds
(fs1 ^ fs2) . e = (Del (fs,a)) . elet e be
Nat;
( 1 <= e & e <= len (Del (fs,a)) implies (fs1 ^ fs2) . e = (Del (fs,a)) . e )assume that A9:
1
<= e
and A10:
e <= len (Del (fs,a))
;
(fs1 ^ fs2) . e = (Del (fs,a)) . enow (fs1 ^ fs2) . e = (Del (fs,a)) . eper cases
( e < a or e >= a )
;
suppose A13:
e >= a
;
(fs1 ^ fs2) . e = (Del (fs,a)) . ethen A14:
e > a - 1
by Lm4;
then A15:
e + 1
> a
by XREAL_1:19;
then
(e + 1) - a > 0
by XREAL_1:50;
then A16:
((e + 1) - a) + 1
> 0 + 1
by XREAL_1:6;
A17:
e + 1
> a - 1
by A15, XREAL_1:146, XXREAL_0:2;
then
(e + 1) - (a - 1) > 0
by XREAL_1:50;
then reconsider f =
(e + 1) - (a - 1) as
Element of
NAT by INT_1:3;
A18:
e + 1
<= len fs
by A4, A10, XREAL_1:6;
then A19:
(e + 1) - (a - 1) <= len (<*v*> ^ fs2)
by A8, XREAL_1:9;
thus (fs1 ^ fs2) . e =
fs2 . (e - (len fs1))
by A3, A5, A10, A14, FINSEQ_1:24
.=
fs2 . (f - 1)
by A3
.=
(<*v*> ^ fs2) . f
by A6, A16, A19, FINSEQ_1:24
.=
(fs1 ^ (<*v*> ^ fs2)) . (e + 1)
by A3, A7, A17, A18, FINSEQ_1:24
.=
(Del (fs,a)) . e
by A1, A7, A13, WSIERP_1:def 1
;
verum end; end; end; hence
(fs1 ^ fs2) . e = (Del (fs,a)) . e
;
verum end;
hence
Del (fs,a) = fs1 ^ fs2
by A5; verum