i,j:
. i
i
j & jiji1,i2,j1,j2:. i1j1 
i2j2 i1i2j1j2a,b:
. ab = ba| Rank | Theorem | Name |
| 2 | i,j:. iij & jij | [factors_bound] |
| cites the following: | ||
| 1 | i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2 | [multiply_functionality_wrt_le] |
| 0 | a,b:. ab = ba | [mul_com] |