let n be Nat; for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let D be non empty set ; for p being Element of D
for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let p be Element of D; for f being FinSequence of D
for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let f be FinSequence of D; for i being Nat st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let i be Nat; ( n + 1 <= i & i <= len f implies (Ins (f,n,p)) . (i + 1) = f . i )
assume that
A1:
n + 1 <= i
and
A2:
i <= len f
; (Ins (f,n,p)) . (i + 1) = f . i
reconsider j = i - (n + 1) as Element of NAT by A1, INT_1:5;
n + (j + 1) <= len f
by A2;
then A3:
j + 1 <= (len f) - n
by XREAL_1:19;
n <= n + 1
by NAT_1:11;
then A4:
n <= i
by A1, XXREAL_0:2;
then
len (f | n) = n
by A2, FINSEQ_1:59, XXREAL_0:2;
then A5:
len ((f | n) ^ <*p*>) = n + 1
by FINSEQ_2:16;
n <= len f
by A2, A4, XXREAL_0:2;
then
( 1 <= j + 1 & j + 1 <= len (f /^ n) )
by A3, NAT_1:11, RFINSEQ:def 1;
then A6:
j + 1 in dom (f /^ n)
by FINSEQ_3:25;
(n + 1) + (j + 1) = i + 1
;
hence (Ins (f,n,p)) . (i + 1) =
(f /^ n) . (j + 1)
by A5, A6, FINSEQ_1:def 7
.=
f . (n + (j + 1))
by A6, Th27
.=
f . i
;
verum