At: add via intseg addends

  a,b:, f,g:({a..b}).
  ( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))

By:

Inst:  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) Using:[ | x,y. x+y | 0]

1	is_commutative_sep(; (x,y. x+y))	1 step
2	is_ident(; (x,y. x+y); 0)	1 step
3	is_assoc_sep(; (x,y. x+y))	1 step
4	1. a,b:, e,g:({a..b}). 1. (x,y. x+y)(( i:{a..b}. e(i)), i:{a..b}. g(i)) 1. = 1. ( i:{a..b}. (x,y. x+y)(e(i),g(i)))   a,b:, f,g:({a..b}).   ( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))	1 step

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