Nuprl - IteratedBinops LEMMAs for add_via_intseg

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

Rank	Theorem	Name
3	Thm* a,b:, f,g:({a..b}). Thm* ( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))	[add_via_intseg_addends]
cites the following:
2	Thm* f:(AAA), u:A. Thm* is_commutative_sep(A; f) Thm* Thm* is_ident(A; f; u) Thm* Thm* is_assoc_sep(A; f) Thm* Thm* (a,b:, e,g:({a..b}A). Thm* (f((Iter(f;u) i:{a..b}. e(i)),Iter(f;u) i:{a..b}. g(i)) Thm* (= Thm* ((Iter(f;u) i:{a..b}. f(e(i),g(i))) Thm* ( A)	[iter_via_intseg_comp_binop]
0	Thm* is_commutative_sep(; (x,y. x+y))	[is_commutative_sep_intadd]
0	Thm* is_ident(; (x,y. x+y); 0)	[intadd_ident_zero]
0	Thm* is_assoc_sep(; (x,y. x+y))	[is_assoc_intadd]

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