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_{1}( 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_{1}(X)
from FUNCT_2:sch 4();

A12: f is one-to-one

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

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

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

A12: f is one-to-one

proof

A18:
rng f c= REAL
by RELAT_1:def 19;
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_{1}(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_{1}(a)
by A11, A13;

hence ( not f . a = f . b or a = b ) by A17, A16, A15, Th27; :: thesis: verum

end;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

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

hence ( not f . a = f . b or a = b ) by A17, A16, A15, Th27; :: thesis: verum

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