for p being XFinSequence of NAT st p is dominated_by_0 holds
( <%0%> ^ p is dominated_by_0 & { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} )