let i, k be Element of NAT ; :: thesis: for f being Element of REAL *
for r being Real st i <> k & i in dom f holds
(f,i := k,r) . i = k
let f be Element of REAL * ; :: thesis: for r being Real st i <> k & i in dom f holds
(f,i := k,r) . i = k
let r be Real; :: thesis: ( i <> k & i in dom f implies (f,i := k,r) . i = k )
assume that
A1: i <> k and
A2: i in dom f ; :: thesis: (f,i := k,r) . i = k
set fik = f,i := k;
thus (f,i := k,r) . i = (f,i := k) . i by A1, FUNCT_7:34
.= k by A2, FUNCT_7:33 ; :: thesis: verum