Nuprl - IteratedBinops LEMMAs for mul_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))	[mul_via_intseg_factors]
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. xy))	[is_commutative_sep_intmul]
0	Thm* is_ident(; (x,y. xy); 1)	[intmul_ident_one]
0	Thm* is_assoc_sep(; (x,y. xy))	[is_assoc_intmul]

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