:: deftheorem defines SolutionsOfSumOfReciprocals NUMBER17:def 7 :
for s being Nat holds SolutionsOfSumOfReciprocals s = { f where f is b₁ -element natural-valued positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } ;