defpred S_{1}[ object , object ] means ex i being Integer ex n being Nat st

( $1 = [i,n] & $2 = i / n );

A1: for a being object st a in [:INT,NAT:] holds

ex b being object st S_{1}[a,b]

A5: ( dom f = [:INT,NAT:] & ( for a being object st a in [:INT,NAT:] holds

S_{1}[a,f . a] ) )
from CLASSES1:sch 1(A1);

A6: RAT c= rng f

.= omega by CARD_2:def 2, CARD_4:6 ;

hence card RAT c= omega by A5, A6, CARD_1:12; :: according to XBOOLE_0:def 10 :: thesis: omega c= card RAT

thus omega c= card RAT by CARD_1:11, CARD_1:47, NUMBERS:18; :: thesis: verum

( $1 = [i,n] & $2 = i / n );

A1: for a being object st a in [:INT,NAT:] holds

ex b being object st S

proof

consider f being Function such that
let a be object ; :: thesis: ( a in [:INT,NAT:] implies ex b being object st S_{1}[a,b] )

assume a in [:INT,NAT:] ; :: thesis: ex b being object st S_{1}[a,b]

then consider x, y being object such that

A2: x in INT and

A3: y in NAT and

A4: a = [x,y] by ZFMISC_1:def 2;

reconsider y = y as Nat by A3;

reconsider x = x as Integer by A2;

x / y = x / y ;

hence ex b being object st S_{1}[a,b]
by A4; :: thesis: verum

end;assume a in [:INT,NAT:] ; :: thesis: ex b being object st S

then consider x, y being object such that

A2: x in INT and

A3: y in NAT and

A4: a = [x,y] by ZFMISC_1:def 2;

reconsider y = y as Nat by A3;

reconsider x = x as Integer by A2;

x / y = x / y ;

hence ex b being object st S

A5: ( dom f = [:INT,NAT:] & ( for a being object st a in [:INT,NAT:] holds

S

A6: RAT c= rng f

proof

card [:INT,NAT:] =
card [:omega,omega:]
by Th16, CARD_2:7
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in RAT or a in rng f )

assume a in RAT ; :: thesis: a in rng f

then consider i, j being Integer such that

A7: a = i / j by RAT_1:def 1;

consider n being Nat such that

A8: ( j = n or j = - n ) by INT_1:2;

i / (- n) = - (i / n) by XCMPLX_1:188;

then ( a = i / n or a = (- i) / n ) by A7, A8, XCMPLX_1:187;

then consider k being Integer such that

A9: a = k / n ;

( k in INT & n in NAT ) by INT_1:def 2, ORDINAL1:def 12;

then A10: [k,n] in [:INT,NAT:] by ZFMISC_1:def 2;

then consider i1 being Integer, n1 being Nat such that

A11: [k,n] = [i1,n1] and

A12: f . [k,n] = i1 / n1 by A5;

A13: n = n1 by A11, XTUPLE_0:1;

i1 = k by A11, XTUPLE_0:1;

hence a in rng f by A13, A5, A9, A10, A12, FUNCT_1:def 3; :: thesis: verum

end;assume a in RAT ; :: thesis: a in rng f

then consider i, j being Integer such that

A7: a = i / j by RAT_1:def 1;

consider n being Nat such that

A8: ( j = n or j = - n ) by INT_1:2;

i / (- n) = - (i / n) by XCMPLX_1:188;

then ( a = i / n or a = (- i) / n ) by A7, A8, XCMPLX_1:187;

then consider k being Integer such that

A9: a = k / n ;

( k in INT & n in NAT ) by INT_1:def 2, ORDINAL1:def 12;

then A10: [k,n] in [:INT,NAT:] by ZFMISC_1:def 2;

then consider i1 being Integer, n1 being Nat such that

A11: [k,n] = [i1,n1] and

A12: f . [k,n] = i1 / n1 by A5;

A13: n = n1 by A11, XTUPLE_0:1;

i1 = k by A11, XTUPLE_0:1;

hence a in rng f by A13, A5, A9, A10, A12, FUNCT_1:def 3; :: thesis: verum

.= omega by CARD_2:def 2, CARD_4:6 ;

hence card RAT c= omega by A5, A6, CARD_1:12; :: according to XBOOLE_0:def 10 :: thesis: omega c= card RAT

thus omega c= card RAT by CARD_1:11, CARD_1:47, NUMBERS:18; :: thesis: verum