let i, n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let p be Element of D; :: thesis: for f being FinSequence of D st n + 1 <= i & i <= len f holds
(Ins (f,n,p)) . (i + 1) = f . i
let f be FinSequence of D; :: thesis: ( 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 ; :: thesis: (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 ;
:: thesis: verum