let m, n be Nat; :: thesis: 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 ) )
let p be XFinSequence of NAT ; :: thesis: ( p in Domin_0 (n,m) iff ( p is dominated_by_0 & dom p = n & Sum p = m ) )
thus ( p in Domin_0 (n,m) implies ( p is dominated_by_0 & dom p = n & Sum p = m ) ) :: thesis: ( p is dominated_by_0 & dom p = n & Sum p = m implies p in Domin_0 (n,m) )

proof

assume p in Domin_0 (n,m) ; :: thesis: ( p is dominated_by_0 & dom p = n & Sum p = m )
then ex q being XFinSequence of NAT st
( q = p & q is dominated_by_0 & dom q = n & Sum q = m ) by Def2;
hence ( p is dominated_by_0 & dom p = n & Sum p = m ) ; :: thesis: verum

end;

thus ( p is dominated_by_0 & dom p = n & Sum p = m implies p in Domin_0 (n,m) ) by Def2; :: thesis: verum