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); 0)| Theorem | Name |
| a,b:, e:({a..b}). a+1 = b ( i:{a..b}. e(i)) = e(a) | [sum_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. x+y); 0) | [intadd_ident_zero] |