a,b:
, e:({a..b
}
). a+1 = b 
(
i:{a..b}. e(i)) = e(a)f:(AAA), u:A.
Thm* is_ident(A; f; u)
Thm*
Thm* (
a,b:, e:({a..b}A). a+1 = b (Iter(f;u) i:{a..b}. e(i)) = e(a)); (
x,y. x
y); 1)| Theorem | Name |
| a,b:, e:({a..b}). a+1 = b ( i:{a..b}. e(i)) = e(a) | [mul_via_intseg_singleton] |
| cites the following: | |
| f:(AAA), u:A.
Thm* is_ident(A; f; u) Thm*
Thm* ( a,b:, e:({a..b}A). a+1 = b (Iter(f;u) i:{a..b}. e(i)) = e(a)) | [iter_via_intseg_singleton] |
| ; (x,y. xy); 1) | [intmul_ident_one] |