a,a':
.
Thm* a'-a = 1
(B:({a..a'
}
Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))a,a':. a'-a = 1 ({a..a'} =ext {a:})| Theorem | Name |
| a,a':.
Thm* a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a))) | [exteq_prod_family_singleton_vs_intseg] |
| cites the following: | |
| a,a':. a'-a = 1 ({a..a'} =ext {a:}) | [exteq_singleton_vs_intseg] |