for n, k being Nat ex p being XFinSequence of NAT st
( Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) & dom p = k + 1 & ( for i being Nat st i <= k holds
p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) )