defpred S₁[ 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₁[a,b]

let a be object ; :: thesis:
assume a in [:INT,NAT:] ; :: thesis:
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₁[a,b] by A4; :: thesis:

end;

consider f being Function such that
A5: ( dom f = [:INT,NAT:] & ( for a being object st a in [:INT,NAT:] holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
A6: RAT c= rng f

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in RAT ; :: thesis:
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:

end;