let n be Nat; :: thesis: ( n > 0 implies Domin_0 ((2 * n),n) = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } )
assume A1: n > 0 ; :: thesis: Domin_0 ((2 * n),n) = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) }
set P = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } ;
thus Domin_0 ((2 * n),n) c= { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } :: according to XBOOLE_0:def 10 :: thesis: { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } c= Domin_0 ((2 * n),n)

proof

A2: n + n > 0 + 0 by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Domin_0 ((2 * n),n) or x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } )
assume A3: x in Domin_0 ((2 * n),n) ; :: thesis: x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) }
consider p being XFinSequence of NAT such that
A4: x = p and
p is dominated_by_0 and
A5: ( dom p = 2 * n & Sum p = n ) by A3, Def2;
A6: p in NAT ^omega by AFINSQ_1:def 7;
2 * (Sum (p | (2 * n))) = 2 * n by A5;
then 2 * n in { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } by A2;
hence x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } by A3, A4, A6; :: thesis: verum

end;

thus { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } c= Domin_0 ((2 * n),n) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } or x in Domin_0 ((2 * n),n) )
assume x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } ; :: thesis: x in Domin_0 ((2 * n),n)
then ex pN being Element of NAT ^omega st
( x = pN & pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) ;
hence x in Domin_0 ((2 * n),n) ; :: thesis: verum

end;