 These two functions are clearly extensionally equivalent: they assign the same value to the same input at the actual world. Moreover, given standard assumptions in possible worlds semantics, the two functions are also intensionally equivalent. If we assume that mathematical facts, like facts about addition and subtraction, are necessary in the sense that they are the same at every possible world, then we get that the two functions give the same value to the arguments at every possible world. So, an intensional function concept would require the two functions to be identical. In the \(\lambda\)-calculus, however, it’s not clear at all that we should identify the two functions. Formally speaking, without the help of other principle, we cannot show that the two \(\lambda\)-terms denote the same function. Moreover, informally speaking, on the conception of functions-as-rules, it’s not even clear that we should identify them: the two terms involve genuinely different rules, and so we might be tempted to say that they denote different functions.