let D be non empty set ; for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
let f be FinSequence of D; for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
let p be Element of D; for i being Nat st 1 <= i & i <= len f holds
(Replace (f,i,p)) . i = p
let i be Nat; ( 1 <= i & i <= len f implies (Replace (f,i,p)) . i = p )
assume
( 1 <= i & i <= len f )
; (Replace (f,i,p)) . i = p
then
i in dom f
by FINSEQ_3:25;
hence
(Replace (f,i,p)) . i = p
by FUNCT_7:31; verum