let f be FinSequence; 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; 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 ; ( 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 )
; (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; verum