not [0,0] in RAT+ by ARYTM_3:33;
then A1: RAT = RAT+ \/ ([:{0},RAT+:] \ {[0,0]}) by NUMBERS:def 3, XBOOLE_1:87, ZFMISC_1:50;
then bool RAT+ c= bool RAT by XBOOLE_1:7, ZFMISC_1:67;
then A2: DEDEKIND_CUTS c= bool RAT ;
RAT+ c= RAT by A1, XBOOLE_1:7;
then RAT+ \/ DEDEKIND_CUTS c= RAT \/ (bool RAT) by A2, XBOOLE_1:13;
then REAL+ c= RAT \/ (bool RAT) by ARYTM_2:def 2;
then A3: card REAL+ c= card (RAT \/ (bool RAT)) by CARD_1:11;
set INFNAT = (bool NAT) \ (Fin NAT);
A4: card RAT in card (bool RAT) by CARD_1:14;
card (RAT \/ (bool RAT)) c= (card RAT) +` (card (bool RAT)) by CARD_2:34;
then card REAL+ c= (card RAT) +` (card (bool RAT)) by A3;
then card REAL+ c= card (bool RAT) by A4, CARD_2:76;
then card REAL+ c= exp (2,omega) by Th17, CARD_2:31;
then (card REAL+) +` (card REAL+) c= (exp (2,omega)) +` (exp (2,omega)) by CARD_2:83;
then A5: (card REAL+) +` (card REAL+) c= exp (2,omega) by CARD_2:76;
deffunc H<sub>1</sub>( set ) -> Element of REAL = In ((Sum ($1 -powers (1 / 2))),REAL);
A6: card [:{0},REAL+:] = card [:REAL+,{0}:] by CARD_2:4
.= card REAL+ by CARD_1:69 ;
A7: continuum c= card (REAL+ \/ [:{0},REAL+:]) by CARD_1:11, NUMBERS:def 1;
card (REAL+ \/ [:{0},REAL+:]) c= (card REAL+) +` (card [:{0},REAL+:]) by CARD_2:34;
then continuum c= (card REAL+) +` (card REAL+) by A7, A6;
hence continuum c= exp (2,omega) by A5; :: according to XBOOLE_0:def 10 :: thesis: exp (2,omega) c= continuum
Fin NAT is countable by Th28, CARD_4:2;
then A8: card (Fin NAT) c= omega ;
then card (Fin NAT) in card (bool NAT) by CARD_1:14, CARD_1:47, ORDINAL1:12;
then A9: (card (bool NAT)) +` (card (Fin NAT)) = card (bool NAT) by CARD_2:76;
A10: omega in card (bool NAT) by CARD_1:14, CARD_1:47;
then reconsider INFNAT = (bool NAT) \ (Fin NAT) as non empty set by A8, CARD_1:68, ORDINAL1:12;
consider f being Function of INFNAT,REAL such that
A11: for X being Element of INFNAT holds f . X = H₁(X) from FUNCT_2:sch 4();
A12: f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A13: a in dom f and
A14: b in dom f ; :: thesis: ( not f . a = f . b or a = b )
reconsider a = a, b = b as set by TARSKI:1;
A15: f . b = H₁(b) by A11, A14;
not b in Fin NAT by A14, XBOOLE_0:def 5;
then A16: b is infinite Subset of NAT by A14, FINSUB_1:def 5, XBOOLE_0:def 5;
not a in Fin NAT by A13, XBOOLE_0:def 5;
then A17: a is infinite Subset of NAT by A13, FINSUB_1:def 5, XBOOLE_0:def 5;
f . a = H₁(a) by A11, A13;
hence ( not f . a = f . b or a = b ) by A17, A16, A15, Th27; :: thesis: verum

end;

A18: rng f c= REAL by RELAT_1:def 19;
dom f = INFNAT by FUNCT_2:def 1;
then card INFNAT c= continuum by A12, A18, CARD_1:10;
then card (bool NAT) c= continuum by A9, A8, A10, CARD_2:98, ORDINAL1:12;
hence exp (2,omega) c= continuum by CARD_1:47, CARD_2:31; :: thesis: verum