let f be FinSequence; :: thesis: for i, j being Nat
for a, b being object st i in dom f & j in dom f & i <> j holds
(Replace (f,i,j,a,b)) . i = a
let i, j be Nat; :: thesis: for a, b being object st i in dom f & j in dom f & i <> j holds
(Replace (f,i,j,a,b)) . i = a
let a, b be object ; :: thesis: ( i in dom f & j in dom f & i <> j implies (Replace (f,i,j,a,b)) . i = a )
set g = Replace (f,i,j,a,b);
assume A1: ( i in dom f & j in dom f & i <> j ) ; :: thesis: (Replace (f,i,j,a,b)) . i = a
then (Replace (f,i,j,a,b)) . i = (f +* (i,a)) . i by FUNCT_7:32
.= a by A1, FUNCT_7:31 ;
hence (Replace (f,i,j,a,b)) . i = a ; :: thesis: verum