for m, n being Nat
for p being XFinSequence of NAT holds
( p in Domin_0 (n,m) iff ( p is dominated_by_0 & dom p = n & Sum p = m ) )