a,b:
, f,g:({a..b
}
), j:{a..b}.
0<f(j)
0<g(j) reduce_factorization(f; j) = reduce_factorization(g; j) f = g a,b:, f,g:({a..b}), j:{a..b}.
0<f(j)
0<g(j) reduce_factorization(f; j) = reduce_factorization(g; j) f = g| By: |
THEN FunExtensionality |
| 1 |
2. b :
3. f : {a..b }
4. g : {a..b }
5. j : {a..b }
6. 0<f(j) 7. 0<g(j) 8. reduce_factorization(f; j) = reduce_factorization(g; j) 9. x : {a..b }
f(x) = g(x) | 3 steps |
About:
 |  |  |  |  |  |  |  |