a:{2...}, b:
, f:({a..b
}
). 
{a..b}(f) = 1 
(i:{a..b}. f(i) = 0)e:({a..b}). ( i:{a..b}. e(i)) = 1 (i:{a..b}. e(i) = 1)| Rank | Theorem | Name |
| 5 | a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 (i:{a..b}. f(i) = 0) | [eval_factorization_one] |
| cites the following: | ||
| 4 | e:({a..b}). ( i:{a..b}. e(i)) = 1 (i:{a..b}. e(i) = 1) | [iter_nat_prod_one_iff_factors_one] |