let n be Element of 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 & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 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 & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) }
set P = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (2 * n),n & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } ;
thus Domin_0 (2 * n),n c= { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (2 * n),n & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } :: according to XBOOLE_0:def 10 :: thesis: { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (2 * n),n & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } c= Domin_0 (2 * n),n

proof

let x be set ; :: 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 & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } )
assume A2: 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 & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) }
consider p being XFinSequence of such that
A3: ( x = p & p is dominated_by_0 & dom p = 2 * n & Sum p = n ) by A2, Def2;
( 2 * (Sum (p | (2 * n))) = 2 * n & n + n > 0 + 0 ) by A1, A3, RELAT_1:98;
then ( 2 * n in { i where i is Element of NAT : ( 2 * (Sum (p | i)) = i & i > 0 ) } & p in NAT ^omega ) by AFINSQ_1:def 8;
hence x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (2 * n),n & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } by A2, A3; :: thesis: verum

end;

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

proof

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

end;