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;
( k <> i & k in dom f ) by A1, FINSEQ_3:27;
hence (Replace f,i,p) /. k = f /. k by FUNCT_7:39; :: thesis: verum