let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i, k 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 i, k 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 i, k being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k
let i, k 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 12;
( k <> i & k in dom f ) by A1, FINSEQ_3:25;
hence (Replace (f,i,p)) /. k = f /. k by FUNCT_7:37; :: thesis: verum