# Re: [isabelle] Equal on function objects

```John Munroe wrote:
```
```Hi,

I'm trying to show that two function objects are equal in the following:

theory T1
imports Real
begin

typedecl T

consts
func1 :: "T => real"
func2 :: "T => real"
func3 :: "T => real"

locale loc =
assumes ax1: "func1 p = func2 p / func3 p"
and ax2: "func3 p > 0"

lemma (in loc) lem1: "ALL p. func2 p = func1 p * func3 p"
using ax1 ax2
by (metis divide_le_eq divide_less_eq order_eq_refl order_less_irrefl xt1(11))

lemma (in loc) lem2:
assumes "loc"
shows "func2 = (%s. func1 s * func3 s)"
using lem1
by auto

Does anyone know why having lem1 as a fact is insufficient to complete
the proof?
```
```
Try rule 'ext', specifically by (auto intro: ext)
by (blast intro: ext) also solves it

```
Isabelle doesn't apply ext within auto by default, possibly as it can lead to explosions with recursive functions.
```
Sincerely,

Rafal Kolanski.

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.