let i, k, m be Nat; :: thesis: for f being Element of REAL *

for r being Real st m <> i & m <> k holds

((f,i) := (k,r)) . m = f . m

let f be Element of REAL * ; :: thesis: for r being Real st m <> i & m <> k holds

((f,i) := (k,r)) . m = f . m

let r be Real; :: thesis: ( m <> i & m <> k implies ((f,i) := (k,r)) . m = f . m )

assume that

A1: m <> i and

A2: m <> k ; :: thesis: ((f,i) := (k,r)) . m = f . m

set fik = (f,i) := k;

thus ((f,i) := (k,r)) . m = ((f,i) := k) . m by A2, FUNCT_7:32

.= f . m by A1, FUNCT_7:32 ; :: thesis: verum

for r being Real st m <> i & m <> k holds

((f,i) := (k,r)) . m = f . m

let f be Element of REAL * ; :: thesis: for r being Real st m <> i & m <> k holds

((f,i) := (k,r)) . m = f . m

let r be Real; :: thesis: ( m <> i & m <> k implies ((f,i) := (k,r)) . m = f . m )

assume that

A1: m <> i and

A2: m <> k ; :: thesis: ((f,i) := (k,r)) . m = f . m

set fik = (f,i) := k;

thus ((f,i) := (k,r)) . m = ((f,i) := k) . m by A2, FUNCT_7:32

.= f . m by A1, FUNCT_7:32 ; :: thesis: verum