Nuprl - Proof: compose iter sum comp rw

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter sum comp rw

A:Type, f:(A

A), k:

, i:{0...k}. f{

k} = f{

i} o f{

k-i}

By:	Def of <fun> o <fun> THEN FunExtensionality

Generated subgoal:

1 1. A : Type
2. f : AA
3. k :
4. i : {0...k}
5. x : A
f{k}(x) = f{i}(f{k-i}(x))
1 step

About:

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