IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm*  a,b:e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)[mul_via_intseg_singleton]
cites the following:
Thm*  f:(AAA), u:A.
Thm*  is_ident(Afu)
Thm*  
Thm*  (a,b:e:({a..b}A). a+1 = b  (Iter(f;ui:{a..b}. e(i)) = e(a))
[iter_via_intseg_singleton]
Thm*  is_ident(; (x,yxy); 1)[intmul_ident_one]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops Sections DiscrMathExt Doc