let n, m be Nat; :: thesis: ( 2 * m <= n implies ex CardF being XFinSequence of NAT 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 NAT 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 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 Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } c= Domin_0 (n,m)

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 (n,m) & { N where N is 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 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 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 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 Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } c= Domin_0 (n,m)

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 (n,m) & { N where N is 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 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 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 Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } as finite set by A2;
consider C being XFinSequence of NAT 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, Th37;
reconsider Ze = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is 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 object 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 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 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 object ; :: 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 NAT 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 7;
set I = { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } ;

now :: thesis: x in Ze \/ Zne

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

suppose { N where N is 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 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;

now :: thesis: card (Domin_0 (n,m)) = (Sum C) + (card (Domin_0 ((n -' 1),m)))

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 Nat by NAT_1:20;
n = n1 + 1 ;
then A18: card Ze = card (Domin_0 (n1,m)) by Th40;
n1 = n -' 1 by A17, NAT_1:14, XREAL_1:233;
hence card (Domin_0 (n,m)) = (Sum C) + (card (Domin_0 ((n -' 1),m))) by A7, A14, A4, A18, CARD_2:40; :: 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