for x being REAL -valued FinSequence st x is positive holds
for i being Nat
for s being Real st 1 <= i & i < len x holds
(Q_ex x) . ((i + 1),s) = ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1))))))