Def ij == ji

is mentioned by

Thm* n:. n2  (A^n) = A(A^(n-1))	[sfa_doc_ntuple_is_prod]
Def  u in X: A^n. P(u) Def == n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u))) Def (recursive)	[sfa_doc_ntuple_contains]

In prior sections: int 2 list 1

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