let i, k be 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:30

.= dom f by FUNCT_7:30 ; :: thesis: verum

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:30

.= dom f by FUNCT_7:30 ; :: thesis: verum