a,b:
, e:({a..b
}
). (i:{a..b}. e(i) = 1) 
(
i:{a..b}. e(i)) = 1f:(AAA), u:A.
Thm* is_ident(A; f; u)
Thm*
Thm* (
a,b:, e:({a..b}A).
Thm* ((
i:{a..b}. e(i) = u) (Iter(f;u) i:{a..b}. e(i)) = u); (
x,y. x
y); 1)| Rank | Theorem | Name |
| 3 | a,b:, e:({a..b}). (i:{a..b}. e(i) = 1) ( i:{a..b}. e(i)) = 1 | [mul_via_intseg_one] |
| cites the following: | ||
| 2 | f:(AAA), u:A.
Thm* is_ident(A; f; u) Thm*
Thm* ( a,b:, e:({a..b}A).
Thm* (( i:{a..b}. e(i) = u) (Iter(f;u) i:{a..b}. e(i)) = u) | [iter_via_intseg_all_units] |
| 0 | ; (x,y. xy); 1) | [intmul_ident_one] |