let k, i be Element of NAT ; :: thesis: for f being Element of REAL *
for r being Real st k in dom f holds
(f,i := k,r) . k = r
let f be Element of REAL * ; :: thesis: for r being Real st k in dom f holds
(f,i := k,r) . k = r
let r be Real; :: thesis: ( k in dom f implies (f,i := k,r) . k = r )
set fik = f,i := k;
A1: dom (f,i := k) = dom f by FUNCT_7:32;
assume k in dom f ; :: thesis: (f,i := k,r) . k = r
hence (f,i := k,r) . k = r by A1, FUNCT_7:33; :: thesis: verum