for n, m being Nat st 2 * m <= n holds
ex CardF being XFinSequence of NAT st
( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardF & dom CardF = m & ( for j being Nat st j < m holds
CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) )