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