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:80;
then len ((f | n) ^ <*p*>) = n + 1 by FINSEQ_2:19;
then n + 1 in dom ((f | n) ^ <*p*>) by A1, FINSEQ_3:27;
hence (Ins f,n,p) /. (n + 1) = ((f | n) ^ <*p*>) /. (n + 1) by Lm1
.= p by A2, FINSEQ_4:82 ;
:: thesis: verum