let n, m be Element of NAT ; :: thesis: card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } = card (Domin_0 n,m)
set F = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } ;
set Z = Domin_0 n,m;
defpred S1[ set , set ] means ex p being XFinSequence of st
( $1 = <%0 %> ^ p & $2 = p );
A1:
for x being set st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } holds
ex y being set st
( y in Domin_0 n,m & S1[x,y] )
proof
let x be
set ;
:: thesis: ( x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } implies ex y being set st
( y in Domin_0 n,m & S1[x,y] ) )
assume
x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) }
;
:: thesis: ex y being set st
( y in Domin_0 n,m & S1[x,y] )
then consider pN being
Element of
NAT ^omega such that A2:
(
x = pN &
pN in Domin_0 (n + 1),
m &
{ i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} )
;
(
pN is
dominated_by_0 &
dom pN = n + 1 &
len pN = dom pN )
by A2, Th24;
then consider q being
XFinSequence of
such that A3:
(
pN = <%0 %> ^ q &
q is
dominated_by_0 )
by A2, Th21;
take
q
;
:: thesis: ( q in Domin_0 n,m & S1[x,q] )
(
Sum pN = (Sum <%0 %>) + (Sum q) &
Sum <%0 %> = 0 )
by A3, Lm4, STIRL2_1:44;
then A4:
Sum q = m
by A2, Th24;
(
dom pN = (len <%0 %>) + (len q) &
len <%0 %> = 1 )
by A3, AFINSQ_1:36, AFINSQ_1:def 4;
then
n + 1
= (len q) + 1
by A2, Th24;
then
dom q = n
;
hence
(
q in Domin_0 n,
m &
S1[
x,
q] )
by A2, A3, A4, Th24;
:: thesis: verum
end;
consider f being Function of { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } ,(Domin_0 n,m) such that
A5:
for x being set st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
A6:
( Domin_0 n,m = {} implies { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } = {} )
proof
assume A7:
Domin_0 n,
m = {}
;
:: thesis: { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } = {}
assume
{ pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } <> {}
;
:: thesis: contradiction
then consider x being
set such that A8:
x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) }
by XBOOLE_0:def 1;
consider pN being
Element of
NAT ^omega such that A9:
(
x = pN &
pN in Domin_0 (n + 1),
m &
{ i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} )
by A8;
dom pN = n + 1
by A9, Th24;
then
pN | (n + 1) = pN
by RELAT_1:98;
then A10:
(
Sum (pN | (n + 1)) = m &
pN is
dominated_by_0 & 2
* m > n )
by A7, A9, Th24, Th26;
then
( 2
* m <= n + 1 & 2
* m >= n + 1 )
by Th6, NAT_1:13;
then
2
* (Sum (pN | (n + 1))) = n + 1
by A10, XXREAL_0:1;
then
n + 1
in { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) }
;
hence
contradiction
by A9;
:: thesis: verum
end;
then A11:
dom f = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) }
by FUNCT_2:def 1;
for x, y being set st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } & y in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } & f . x = f . y holds
x = y
then A13:
f is one-to-one
by A6, FUNCT_2:25;
rng f = Domin_0 n,m
proof
thus
rng f c= Domin_0 n,
m
;
:: according to XBOOLE_0:def 10 :: thesis: Domin_0 n,m c= rng f
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Domin_0 n,m or x in rng f )
assume A14:
x in Domin_0 n,
m
;
:: thesis: x in rng f
consider p being
XFinSequence of
such that A15:
(
p = x &
p is
dominated_by_0 &
dom p = n &
Sum p = m )
by A14, Def2;
set q =
<%0 %> ^ p;
(
dom (<%0 %> ^ p) = (len <%0 %>) + (len p) &
len p = dom p &
Sum (<%0 %> ^ p) = (Sum <%0 %>) + (Sum p) )
by Lm4, AFINSQ_1:def 4;
then
(
dom (<%0 %> ^ p) = 1
+ n &
Sum (<%0 %> ^ p) = 0 + m &
<%0 %> ^ p is
dominated_by_0 )
by A15, Th22, AFINSQ_1:36, STIRL2_1:44;
then
(
<%0 %> ^ p in Domin_0 (n + 1),
m &
{ i where i is Element of NAT : ( 2 * (Sum ((<%0 %> ^ p) | i)) = i & i > 0 ) } = {} &
<%0 %> ^ p in NAT ^omega )
by A15, Th22, Th24, AFINSQ_1:def 8;
then A16:
<%0 %> ^ p in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) }
;
then consider r being
XFinSequence of
such that A17:
(
<%0 %> ^ p = <%0 %> ^ r &
f . (<%0 %> ^ p) = r )
by A5;
r = p
by A17, AFINSQ_1:31;
hence
x in rng f
by A11, A15, A16, A17, FUNCT_1:12;
:: thesis: verum
end;
then
{ pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } , Domin_0 n,m are_equipotent
by A11, A13, WELLORD2:def 4;
hence
card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } = card (Domin_0 n,m)
by CARD_1:21; :: thesis: verum