Description: A definition of function value in terms of iota, analogous to dffv3 . (Contributed by AV, 6-Sep-2022)