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

.= k by A2, FUNCT_7:31 ; :: thesis: verum

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:32

.= k by A2, FUNCT_7:31 ; :: thesis: verum