IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm*  a,c,b:e:({a..b}).
Thm*  ac
Thm*  
Thm*  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))
[mul_via_intseg_split_mid]
cites the following:
2Thm*  f:(AAA), u:A.
Thm*  is_ident(Afu)
Thm*  
Thm*  is_assoc_sep(Af)
Thm*  
Thm*  (a,c,b:e:({a..b}A).
Thm*  (ac
Thm*  (
Thm*  (cb
Thm*  (
Thm*  ((Iter(f;ui:{a..b}. e(i))
Thm*  (=
Thm*  (f((Iter(f;ui:{a..c}. e(i)),Iter(f;ui:{c..b}. e(i)))
[iter_via_intseg_split_mid]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops Sections DiscrMathExt Doc