let n, m be Nat; :: thesis: ( 2 * m <= n implies ex CardF being XFinSequence of st
( card (Domin_0 n,m) = (Sum CardF) + (card (Domin_0 (n -' 1),m)) & dom CardF = m & ( for j being Nat st j < m holds
CardF . j = (card (Domin_0 (2 * j),j)) * (card (Domin_0 (n -' (2 * (j + 1))),(m -' (j + 1)))) ) ) )
assume A1: 2 * m <= n ; :: thesis: ex CardF being XFinSequence of st
( card (Domin_0 n,m) = (Sum CardF) + (card (Domin_0 (n -' 1),m)) & dom CardF = m & ( for j being Nat st j < m holds
CardF . j = (card (Domin_0 (2 * j),j)) * (card (Domin_0 (n -' (2 * (j + 1))),(m -' (j + 1)))) ) )
set Z = Domin_0 n,m;
set Zne = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } ;
A2: { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } c= Domin_0 n,m

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 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } or x in Domin_0 n,m )
assume x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } ; :: thesis: x in Domin_0 n,m
then ex pN being Element of NAT ^omega st
( x = pN & pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) ;
hence x in Domin_0 n,m ; :: thesis: verum

end;

set Ze = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } ;
A3: { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } c= Domin_0 n,m

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 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } or x in Domin_0 n,m )
assume x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } ; :: thesis: x in Domin_0 n,m
then ex pN being Element of NAT ^omega st
( x = pN & pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) ;
hence x in Domin_0 n,m ; :: thesis: verum

end;

reconsider Zne = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } as finite set by A2;
consider C being XFinSequence of such that
A4: card Zne = Sum C and
A5: dom C = m and
A6: for j being Nat st j < m holds
C . j = (card (Domin_0 (2 * j),j)) * (card (Domin_0 (n -' (2 * (j + 1))),(m -' (j + 1)))) by A1, Th41;
reconsider Ze = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } as finite set by A3;
take C ; :: thesis: ( card (Domin_0 n,m) = (Sum C) + (card (Domin_0 (n -' 1),m)) & dom C = m & ( for j being Nat st j < m holds
C . j = (card (Domin_0 (2 * j),j)) * (card (Domin_0 (n -' (2 * (j + 1))),(m -' (j + 1)))) ) )
A7: Ze misses Zne

proof

assume Ze meets Zne ; :: thesis: contradiction
then consider x being set such that
A8: x in Ze and
A9: x in Zne by XBOOLE_0:3;
A10: ex qN being Element of NAT ^omega st
( qN = x & qN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (qN | N)) = N & N > 0 ) } = {} ) by A8;
ex pN being Element of NAT ^omega st
( pN = x & pN in Domin_0 n,m & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) by A9;
hence contradiction by A10; :: thesis: verum

end;

A11: Domin_0 n,m c= Ze \/ Zne

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Domin_0 n,m or x in Ze \/ Zne )
assume A12: x in Domin_0 n,m ; :: thesis: x in Ze \/ Zne
consider p being XFinSequence of such that
A13: p = x and
p is dominated_by_0 and
dom p = n and
Sum p = m by A12, Def2;
reconsider p = p as Element of NAT ^omega by AFINSQ_1:def 8;
set I = { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } ;

now

per cases ( { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} or { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } <> {} ) ;

suppose { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} ; :: thesis: x in Ze \/ Zne

then p in Ze by A12, A13;
hence x in Ze \/ Zne by A13, XBOOLE_0:def 3; :: thesis: verum

end;

suppose { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } <> {} ; :: thesis: x in Ze \/ Zne

then p in Zne by A12, A13;
hence x in Ze \/ Zne by A13, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in Ze \/ Zne ; :: thesis: verum

end;

Ze \/ Zne c= Domin_0 n,m by A3, A2, XBOOLE_1:8;
then A14: Ze \/ Zne = Domin_0 n,m by A11, XBOOLE_0:def 10;

now

per cases ( n = 0 or n > 0 ) ;

suppose A15: n = 0 ; :: thesis: card (Domin_0 n,m) = (Sum C) + (card (Domin_0 (n -' 1),m))

then 2 * m = 0 by A1;
then C = {} by A5;
then A16: Sum C = 0 ;
n - 1 < 1 - 1 by A15;
hence card (Domin_0 n,m) = (Sum C) + (card (Domin_0 (n -' 1),m)) by A15, A16, XREAL_0:def 2; :: thesis: verum

end;

suppose A17: n > 0 ; :: thesis: card (Domin_0 n,m) = (Sum C) + (card (Domin_0 (n -' 1),m))

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
n = n1 + 1 ;
then A18: card Ze = card (Domin_0 n1,m) by Th44;
n1 = n -' 1 by A17, NAT_1:14, XREAL_1:235;
hence card (Domin_0 n,m) = (Sum C) + (card (Domin_0 (n -' 1),m)) by A7, A14, A4, A18, CARD_2:53; :: thesis: verum

end;

end;

end;

hence ( card (Domin_0 n,m) = (Sum C) + (card (Domin_0 (n -' 1),m)) & dom C = m & ( for j being Nat st j < m holds
C . j = (card (Domin_0 (2 * j),j)) * (card (Domin_0 (n -' (2 * (j + 1))),(m -' (j + 1)))) ) ) by A5, A6; :: thesis: verum