let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace f,i,p) /. k = f /. k
let f be FinSequence of D; :: thesis: for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace f,i,p) /. k = f /. k
let p be Element of D; :: thesis: for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace f,i,p) /. k = f /. k
let k, i be Nat; :: thesis: ( 1 <= k & k <= len f & k <> i implies (Replace f,i,p) /. k = f /. k )
assume A1: ( 1 <= k & k <= len f & k <> i ) ; :: thesis: (Replace f,i,p) /. k = f /. k
reconsider i = i, k = k as Element of NAT by ORDINAL1:def 13;
A2: ( 1 <= k & k <= len f & k <> i ) by A1;
k in dom f by A1, FINSEQ_3:27;
hence (Replace f,i,p) /. k = f /. k by A2, FUNCT_7:39; :: thesis: verum