let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) . (n + 1) = p
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) . (n + 1) = p
let p be Element of D; :: thesis: for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) . (n + 1) = p
let f be FinSequence of D; :: thesis: ( n <= len f implies (Ins (f,n,p)) . (n + 1) = p )
A1: 1 <= n + 1 by NAT_1:11;
assume n <= len f ; :: thesis: (Ins (f,n,p)) . (n + 1) = p
then A2: len (f | n) = n by FINSEQ_1:59;
then len ((f | n) ^ <*p*>) = n + 1 by FINSEQ_2:16;
then n + 1 in dom ((f | n) ^ <*p*>) by A1, FINSEQ_3:25;
hence (Ins (f,n,p)) . (n + 1) = ((f | n) ^ <*p*>) . (n + 1) by Lm1
.= p by A2, FINSEQ_1:42 ;
:: thesis: verum