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)) . j = b
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)) . j = b
let a, b be object ; :: thesis: ( i in dom f & j in dom f & i <> j implies (Replace (f,i,j,a,b)) . j = b )
set g = Replace (f,i,j,a,b);
assume ( i in dom f & j in dom f & i <> j ) ; :: thesis: (Replace (f,i,j,a,b)) . j = b
then j in dom (f +* (i,a)) by FUNCT_7:30;
hence (Replace (f,i,j,a,b)) . j = b by FUNCT_7:31; :: thesis: verum