let i be Nat; for D being non empty set
for f, g being FinSequence of D st i in dom f holds
Del ((f ^ g),i) = (Del (f,i)) ^ g
let D be non empty set ; for f, g being FinSequence of D st i in dom f holds
Del ((f ^ g),i) = (Del (f,i)) ^ g
let f, g be FinSequence of D; ( i in dom f implies Del ((f ^ g),i) = (Del (f,i)) ^ g )
assume A1:
i in dom f
; Del ((f ^ g),i) = (Del (f,i)) ^ g
set Df = Del (f,i);
consider m being Nat such that
A2:
len f = m + 1
and
A3:
len (Del (f,i)) = m
by A1, FINSEQ_3:104;
set Dg = (Del (f,i)) ^ g;
set fg = f ^ g;
set Dfg = Del ((f ^ g),i);
A4:
Seg (len (f ^ g)) = dom (f ^ g)
by FINSEQ_1:def 3;
A5:
len (f ^ g) = (len f) + (len g)
by FINSEQ_1:22;
then
len f <= len (f ^ g)
by NAT_1:12;
then A6:
Seg (len f) c= Seg (len (f ^ g))
by FINSEQ_1:5;
A7:
len (f ^ g) = ((len g) + m) + 1
by A2, A5;
A8:
Seg (len f) = dom f
by FINSEQ_1:def 3;
A9:
now for j being Nat st 1 <= j & j <= m + (len g) holds
((Del (f,i)) ^ g) . j = (Del ((f ^ g),i)) . jlet j be
Nat;
( 1 <= j & j <= m + (len g) implies ((Del (f,i)) ^ g) . j = (Del ((f ^ g),i)) . j )assume that A10:
1
<= j
and A11:
j <= m + (len g)
;
((Del (f,i)) ^ g) . j = (Del ((f ^ g),i)) . jnow (Del ((f ^ g),i)) . j = ((Del (f,i)) ^ g) . jper cases
( j < i or j >= i )
;
suppose A12:
j < i
;
(Del ((f ^ g),i)) . j = ((Del (f,i)) ^ g) . j
i <= len f
by A1, FINSEQ_3:25;
then A13:
j < len f
by A12, XXREAL_0:2;
then A14:
j in dom f
by A10, FINSEQ_3:25;
j <= m
by A2, A13, NAT_1:13;
then A15:
j in dom (Del (f,i))
by A3, A10, FINSEQ_3:25;
thus (Del ((f ^ g),i)) . j =
(f ^ g) . j
by A12, FINSEQ_3:110
.=
f . j
by A14, FINSEQ_1:def 7
.=
(Del (f,i)) . j
by A12, FINSEQ_3:110
.=
((Del (f,i)) ^ g) . j
by A15, FINSEQ_1:def 7
;
verum end; suppose A16:
j >= i
;
((Del (f,i)) ^ g) . j = (Del ((f ^ g),i)) . jnow (Del ((f ^ g),i)) . j = ((Del (f,i)) ^ g) . jper cases
( j <= m or j > m )
;
suppose A17:
j <= m
;
(Del ((f ^ g),i)) . j = ((Del (f,i)) ^ g) . jA18:
0 + 1
<= j + 1
by XREAL_1:7;
j + 1
<= len f
by A2, A17, XREAL_1:7;
then A19:
j + 1
in dom f
by A18, FINSEQ_3:25;
A20:
j in dom (Del (f,i))
by A3, A10, A17, FINSEQ_3:25;
thus (Del ((f ^ g),i)) . j =
(f ^ g) . (j + 1)
by A1, A6, A8, A4, A7, A11, A16, FINSEQ_3:111
.=
f . (j + 1)
by A19, FINSEQ_1:def 7
.=
(Del (f,i)) . j
by A1, A2, A16, A17, FINSEQ_3:111
.=
((Del (f,i)) ^ g) . j
by A20, FINSEQ_1:def 7
;
verum end; suppose A21:
j > m
;
(Del ((f ^ g),i)) . j = ((Del (f,i)) ^ g) . jthen
j >= len f
by A2, NAT_1:13;
then
j + 1
> len f
by NAT_1:13;
then reconsider jL =
(j + 1) - (len f) as
Element of
NAT by NAT_1:21;
j + 1
<= (m + (len g)) + 1
by A11, XREAL_1:7;
then
jL + (len f) <= (len f) + (len g)
by A2;
then A22:
jL <= len g
by XREAL_1:8;
jL <> 0
by A2, A21;
then
jL >= 1
by NAT_1:14;
then A23:
jL in dom g
by A22, FINSEQ_3:25;
thus (Del ((f ^ g),i)) . j =
(f ^ g) . (jL + (len f))
by A1, A6, A8, A4, A7, A11, A16, FINSEQ_3:111
.=
g . jL
by A23, FINSEQ_1:def 7
.=
((Del (f,i)) ^ g) . (m + jL)
by A3, A23, FINSEQ_1:def 7
.=
((Del (f,i)) ^ g) . j
by A2
;
verum end; end; end; hence
((Del (f,i)) ^ g) . j = (Del ((f ^ g),i)) . j
;
verum end; end; end; hence
((Del (f,i)) ^ g) . j = (Del ((f ^ g),i)) . j
;
verum end;
A24:
len ((Del (f,i)) ^ g) = (len (Del (f,i))) + (len g)
by FINSEQ_1:22;
len (Del ((f ^ g),i)) = m + (len g)
by A1, A6, A8, A4, A7, FINSEQ_3:109;
hence
Del ((f ^ g),i) = (Del (f,i)) ^ g
by A3, A24, A9; verum