let i, k be Nat; 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 * ; for r being Real st k in dom f holds
((f,i) := (k,r)) . k = r
let r be Real; ( 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:30;
assume
k in dom f
; ((f,i) := (k,r)) . k = r
hence
((f,i) := (k,r)) . k = r
by A1, FUNCT_7:31; verum