let f be FinSequence; :: thesis: for i, j being Nat
for a, b being object holds dom (Replace (f,i,j,a,b)) = dom f
let i, j be Nat; :: thesis: for a, b being object holds dom (Replace (f,i,j,a,b)) = dom f
let a, b be object ; :: thesis: dom (Replace (f,i,j,a,b)) = dom f
dom (f +* (i,a)) = dom f by FUNCT_7:30;
hence dom (Replace (f,i,j,a,b)) = dom f by FUNCT_7:30; :: thesis: verum