a:
, n:
. 
q:. Div(a;n;q) & (a 
n) = qa:, n:. Div(a;n;a n)a:, n:. (a n) 
| Rank | Theorem | Name |
| 4 | a:, n:. q:. Div(a;n;q) & (a n) = q | [div_elim] |
| cites the following: | ||
| 0 | a:, n:. Div(a;n;a n) | [div_fun_sat_div_nrel] |
| 3 | a:, n:. (a n) | [division_typing1a_sfa] |