let m, n be Nat; card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } = card (Domin_0 (n,m))
defpred S1[ object , object ] means ex p being XFinSequence of NAT st
( $1 = <%0%> ^ p & $2 = p );
set F = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } ;
set Z = Domin_0 (n,m);
A1:
for x being object st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } holds
ex y being object st
( y in Domin_0 (n,m) & S1[x,y] )
proof
A2:
len <%0%> = 1
by AFINSQ_1:33;
let x be
object ;
( x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } implies ex y being object st
( y in Domin_0 (n,m) & S1[x,y] ) )
A3:
Sum <%0%> = 0
by AFINSQ_2:53;
assume
x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) }
;
ex y being object st
( y in Domin_0 (n,m) & S1[x,y] )
then consider pN being
Element of
NAT ^omega such that A4:
(
x = pN &
pN in Domin_0 (
(n + 1),
m) &
{ N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} )
;
(
pN is
dominated_by_0 &
dom pN = n + 1 )
by A4, Th20;
then consider q being
XFinSequence of
NAT such that A6:
pN = <%0%> ^ q
and A7:
q is
dominated_by_0
by A4, Th17;
dom pN = (len <%0%>) + (len q)
by A6, AFINSQ_1:def 3;
then A8:
n + 1
= (len q) + 1
by A4, A2, Th20;
take
q
;
( q in Domin_0 (n,m) & S1[x,q] )
Sum pN = (Sum <%0%>) + (Sum q)
by A6, AFINSQ_2:55;
then
Sum q = m
by A4, A3, Th20;
hence
(
q in Domin_0 (
n,
m) &
S1[
x,
q] )
by A4, A6, A7, A8, Th20;
verum
end;
consider f being Function of { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } ,(Domin_0 (n,m)) such that
A9:
for x being object st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
A10:
( Domin_0 (n,m) = {} implies { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } = {} )
proof
assume
Domin_0 (
n,
m)
= {}
;
{ pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } = {}
then
2
* m > n
by Th22;
then A11:
2
* m >= n + 1
by NAT_1:13;
assume
{ pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } <> {}
;
contradiction
then consider x being
object such that A12:
x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) }
by XBOOLE_0:def 1;
consider pN being
Element of
NAT ^omega such that A13:
(
x = pN &
pN in Domin_0 (
(n + 1),
m) &
{ N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} )
by A12;
dom pN = n + 1
by A13, Th20;
then
pN | (n + 1) = pN
;
then A14:
Sum (pN | (n + 1)) = m
by A13, Th20;
pN is
dominated_by_0
by A13, Th20;
then
2
* m <= n + 1
by A14, Th2;
then
2
* (Sum (pN | (n + 1))) = n + 1
by A14, A11, XXREAL_0:1;
then
n + 1
in { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) }
;
hence
contradiction
by A13;
verum
end;
then A15:
dom f = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) }
by FUNCT_2:def 1;
A16:
rng f = Domin_0 (n,m)
proof
thus
rng f c= Domin_0 (
n,
m)
;
XBOOLE_0:def 10 Domin_0 (n,m) c= rng f
let x be
object ;
TARSKI:def 3 ( not x in Domin_0 (n,m) or x in rng f )
assume
x in Domin_0 (
n,
m)
;
x in rng f
then consider p being
XFinSequence of
NAT such that A17:
p = x
and A18:
p is
dominated_by_0
and A19:
dom p = n
and A20:
Sum p = m
by Def2;
set q =
<%0%> ^ p;
A21:
{ N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {}
by A18, Th18;
Sum (<%0%> ^ p) = (Sum <%0%>) + (Sum p)
by AFINSQ_2:55;
then A22:
Sum (<%0%> ^ p) = 0 + m
by A20, AFINSQ_2:53;
A23:
<%0%> ^ p in NAT ^omega
by AFINSQ_1:def 7;
dom (<%0%> ^ p) = (len <%0%>) + (len p)
by AFINSQ_1:def 3;
then A24:
dom (<%0%> ^ p) = 1
+ n
by A19, AFINSQ_1:33;
<%0%> ^ p is
dominated_by_0
by A18, Th18;
then
<%0%> ^ p in Domin_0 (
(n + 1),
m)
by A24, A22, Th20;
then A25:
<%0%> ^ p in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) }
by A21, A23;
then consider r being
XFinSequence of
NAT such that A26:
<%0%> ^ p = <%0%> ^ r
and A27:
f . (<%0%> ^ p) = r
by A9;
r = p
by A26, AFINSQ_1:28;
hence
x in rng f
by A15, A17, A25, A27, FUNCT_1:3;
verum
end;
for x, y being object st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } & y in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } & f . x = f . y holds
x = y
then
f is one-to-one
by A10, FUNCT_2:19;
then
{ pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } , Domin_0 (n,m) are_equipotent
by A15, A16, WELLORD2:def 4;
hence
card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } = card (Domin_0 (n,m))
by CARD_1:5; verum