let i, k be Element of NAT ; :: thesis: for f being Element of REAL *
for r being Real holds dom (f,i := k,r) = dom f
let f be Element of REAL * ; :: thesis: for r being Real holds dom (f,i := k,r) = dom f
let r be Real; :: thesis: dom (f,i := k,r) = dom f
set fik = f,i := k;
thus dom (f,i := k,r) = dom (f,i := k) by FUNCT_7:32
.= dom f by FUNCT_7:32 ; :: thesis: verum