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

assume k in dom f ; :: thesis: ((f,i) := (k,r)) . k = r

hence ((f,i) := (k,r)) . k = r by A1, FUNCT_7:31; :: thesis: verum

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

assume k in dom f ; :: thesis: ((f,i) := (k,r)) . k = r

hence ((f,i) := (k,r)) . k = r by A1, FUNCT_7:31; :: thesis: verum