'a:S, e:'a, f:('a
'a).
Thm* (
fn1:('a). fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n)))
Thm* & (
fn1,y:('a).
Thm* & (fn1(0) = e & (
n:. fn1(n+1) = f(fn1(n),n))
Thm* & (& y(0) = e
Thm* & (& (
n:. y(n+1) = f(y(n),n))
Thm* & (
Thm* & (fn1 = y)
'a:S.
Thm* all
Thm* (
e:'a. all
Thm* (
e:'a. (f:'a hnum 'a. exists_unique
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. and
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. (equal(fn1(0),e)
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,all
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. equal
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. (fn1(suc(n))
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,f
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,(fn1(n)
Thm* (
e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,,n)))))))