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