:: deftheorem defines exist_subset_sum_eq PRSUBSET:def 2 :
for x being REAL -valued FinSequence
for a being Real holds
( x exist_subset_sum_eq a iff ex I being set st
( I c= dom x & Sum (Seq (x,I)) = a ) );