for s being Real
for x being REAL -valued FinSequence st 1 <= len x holds
(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)