Def  trivial_factorization(z)(i) == if i=z 1 else 0 fi

is mentioned by

Thm*  a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = j	[eval_trivial_factorization]
Thm*  x,y:. x  y  trivial_factorization(x)(y) = 0	[trivial_factorization_comp2]
Thm*  x,y:. x = y  trivial_factorization(x)(y) = 1	[trivial_factorization_comp1]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html