:: deftheorem defQ defines Q_ex PRSUBSET:def 3 :
for x being REAL -valued FinSequence
for b₂ being Function of [:(Seg (len x)),REAL:],BOOLEAN holds
( b₂ = Q_ex x iff for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies b₂ . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b₂ . (i,s) = FALSE ) ) );