A1: card (REAL+ \/ [:{0 },REAL+ :]) c= (card REAL+ ) +` (card [:{0 },REAL+ :]) by CARD_2:47;
A2: card [:{0 },REAL+ :] = card [:REAL+ ,{0 }:] by CARD_2:11
.= card REAL+ by CARD_2:13 ;
not [0 ,0 ] in RAT+ by ARYTM_3:39;
then A3: RAT = RAT+ \/ ([:{0 },RAT+ :] \ {[0 ,0 ]}) by NUMBERS:def 3, XBOOLE_1:87, ZFMISC_1:56;
then A4: RAT+ c= RAT by XBOOLE_1:7;
bool RAT+ c= bool RAT by A3, XBOOLE_1:7, ZFMISC_1:79;
then DEDEKIND_CUTS c= bool RAT by XBOOLE_1:1;
then RAT+ \/ DEDEKIND_CUTS c= RAT \/ (bool RAT ) by A4, XBOOLE_1:13;
then REAL+ c= RAT \/ (bool RAT ) by ARYTM_2:def 2, XBOOLE_1:1;
then ( card REAL+ c= card (RAT \/ (bool RAT )) & card (RAT \/ (bool RAT )) c= (card RAT ) +` (card (bool RAT )) ) by CARD_1:27, CARD_2:47;
then ( card REAL+ c= (card RAT ) +` (card (bool RAT )) & card RAT in card (bool RAT ) ) by CARD_1:30, XBOOLE_1:1;
then card REAL+ c= card (bool RAT ) by CARD_3:118;
then card REAL+ c= exp 2,omega by Th17, CARD_2:44;
then (card REAL+ ) +` (card REAL+ ) c= (exp 2,omega ) +` (exp 2,omega ) by CARD_3:125;
then A5: (card REAL+ ) +` (card REAL+ ) c= exp 2,omega by CARD_3:118;
continuum c= card (REAL+ \/ [:{0 },REAL+ :]) by CARD_1:27, NUMBERS:def 1;
then continuum c= (card REAL+ ) +` (card REAL+ ) by A1, A2, XBOOLE_1:1;
hence continuum c= exp 2,omega by A5, XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: exp 2,omega c= continuum
deffunc H₁( set ) -> Element of REAL = Sum ($1 -powers (1 / 2));
set INFNAT = (bool NAT ) \ (Fin NAT );
Fin NAT is countable by Th28, CARD_4:44;
then A6: ( card (Fin NAT ) c= omega & omega in card (bool NAT ) ) by CARD_1:30, CARD_1:84, CARD_3:def 15;
then A7: card (Fin NAT ) in card (bool NAT ) by ORDINAL1:22;
reconsider INFNAT = (bool NAT ) \ (Fin NAT ) as non empty set by A6, CARD_2:4, ORDINAL1:22;
consider f being Function of INFNAT,REAL such that
A8: for X being Element of INFNAT holds f . X = H₁(X) from FUNCT_2:sch 4();
A9: ( dom f = INFNAT & rng f c= REAL ) by FUNCT_2:def 1, RELAT_1:def 19;
f is one-to-one

proof

let a be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not a in dom f or not b₁ in dom f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume A10: ( a in dom f & b in dom f ) ; :: thesis: ( not f . a = f . b or a = b )
then ( a in bool NAT & not a in Fin NAT & b in bool NAT & not b in Fin NAT ) by XBOOLE_0:def 5;
then ( a is infinite Subset of NAT & b is infinite Subset of NAT & f . a = H₁(a) & f . b = H₁(b) ) by A8, A10, FINSUB_1:def 5;
hence ( not f . a = f . b or a = b ) by Th27; :: thesis: verum

end;

then ( (card (bool NAT )) +` (card (Fin NAT )) = card (bool NAT ) & card INFNAT c= continuum ) by A7, A9, CARD_1:26, CARD_3:118;
then card (bool NAT ) c= continuum by A6, CARD_3:144, ORDINAL1:22;
hence exp 2,omega c= continuum by CARD_1:84, CARD_2:44; :: thesis: verum