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