let m, n be Nat; Domin_0 (n,m) c= Choose (n,m,1,0)
let x be object ; TARSKI:def 3 ( not x in Domin_0 (n,m) or x in Choose (n,m,1,0) )
assume
x in Domin_0 (n,m)
; x in Choose (n,m,1,0)
then consider p being XFinSequence of NAT such that
A1:
p = x
and
A2:
p is dominated_by_0
and
A3:
( dom p = n & Sum p = m )
by Def2;
rng p c= {0,1}
by A2;
hence
x in Choose (n,m,1,0)
by A1, A3, CARD_FIN:40; verum