let f be real-valued FinSequence; :: thesis: for i, j, k being Nat
for a, b being Real st i in dom f & j in dom f & k in dom f & i <> j & k <> i & k <> j holds
(Replace (f,i,j,a,b)) . k = f . k
let i, j, k be Nat; :: thesis: for a, b being Real st i in dom f & j in dom f & k in dom f & i <> j & k <> i & k <> j holds
(Replace (f,i,j,a,b)) . k = f . k
let a, b be Real; :: thesis: ( i in dom f & j in dom f & k in dom f & i <> j & k <> i & k <> j implies (Replace (f,i,j,a,b)) . k = f . k )
assume A1: ( i in dom f & j in dom f & k in dom f & i <> j & k <> i & k <> j ) ; :: thesis: (Replace (f,i,j,a,b)) . k = f . k
(Replace (f,i,j,a,b)) . k = (f +* (i,a)) . k by A1, FUNCT_7:32
.= f . k by A1, FUNCT_7:32 ;
hence (Replace (f,i,j,a,b)) . k = f . k ; :: thesis: verum