let D, E be non empty set ; :: thesis: for d being Element of D

for i being natural Number

for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)

let d be Element of D; :: thesis: for i being natural Number

for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)

let i be natural Number ; :: thesis: for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)

let h be Function of D,E; :: thesis: h * (i |-> d) = i |-> (h . d)

d in D ;

then d in dom h by FUNCT_2:def 1;

hence h * (i |-> d) = i |-> (h . d) by FUNCOP_1:17; :: thesis: verum

for i being natural Number

for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)

let d be Element of D; :: thesis: for i being natural Number

for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)

let i be natural Number ; :: thesis: for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)

let h be Function of D,E; :: thesis: h * (i |-> d) = i |-> (h . d)

d in D ;

then d in dom h by FUNCT_2:def 1;

hence h * (i |-> d) = i |-> (h . d) by FUNCOP_1:17; :: thesis: verum