'a:S, e:'a.
Thm* (
fn:(Unit
'a). fn(
) = e)
Thm* & (
fn,y:(Unit'a). fn() = e & y() = e 
fn = y)'a:S. all(
e:'a. exists_unique(fn:hone 'a. equal(fn(one_el),e)))| Theorem | Name |
| 'a:S, e:'a.
Thm* ( fn:(Unit'a). fn() = e)
Thm* & ( fn,y:(Unit'a). fn() = e & y() = e fn = y) | [one_axiom_2] |
| cites the following: | |
| 'a:S. all(e:'a. exists_unique(fn:hone 'a. equal(fn(one_el),e))) | [hone_axiom_2] |