let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i being Nat holds len (Replace f,i,p) = len f
let f be FinSequence of D; :: thesis: for p being Element of D
for i being Nat holds len (Replace f,i,p) = len f
let p be Element of D; :: thesis: for i being Nat holds len (Replace f,i,p) = len f
let i be Nat; :: thesis: len (Replace f,i,p) = len f
reconsider i = i as Element of NAT by ORDINAL1:def 13;
Seg (len (f +* i,p)) = dom (f +* i,p) by FINSEQ_1:def 3
.= dom f by FUNCT_7:32
.= Seg (len f) by FINSEQ_1:def 3 ;
hence len (Replace f,i,p) = len f by FINSEQ_1:8; :: thesis: verum