Nuprl - IteratedBinops LEMMAs for mul_via_intseg

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
Thm* a,b:, e:({a..b}). Thm* a<b (c:. b = c+1 ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c))	[mul_via_intseg_notnull]
cites the following:
Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* a<b Thm* Thm* (c:. Thm* (b = c+1 Thm* ( Thm* ((Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..c}. e(i)),e(c)))	[iter_via_intseg_notnull]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html