let D, E be non empty set ; :: thesis: for d being Element of D
for i being Nat
for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)
let d be Element of D; :: thesis: for i being Nat
for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)
let i be Nat; :: 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:23; :: thesis: verum