defpred S1[ object , object , object ] means for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st mm = m & n <> 0 & \$1 = m / n & i <> 0 & \$2 = Class ((),[z,i]) holds
\$3 = Class ((),[(mm * z),(n * i)]);
set cF = RAT ;
set C = Class ();
A1: now :: thesis: for q, A being object st q in RAT & A in Class () holds
ex w being object st
( w in Class () & S1[q,A,w] )
let q, A be object ; :: thesis: ( q in RAT & A in Class () implies ex w being object st
( w in Class () & S1[q,A,w] ) )

assume AS0: ( q in RAT & A in Class () ) ; :: thesis: ex w being object st
( w in Class () & S1[q,A,w] )

then consider A1 being object such that
A2: ( A1 in [: the carrier of V,():] & A = Class ((),A1) ) by EQREL_1:def 3;
consider z, i being object such that
A3: ( z in the carrier of V & i in INT \ & A1 = [z,i] ) by ;
reconsider z = z as Element of V by A3;
( i in INT & not i in ) by ;
then A31: ( i in INT & i <> 0 ) by TARSKI:def 1;
reconsider i = i as Integer by A3;
consider m, n being Integer such that
A4: ( n <> 0 & q = m / n ) by ;
reconsider I = i, mn = m, no = n as Element of INT.Ring by Lem1;
A61: not no * i in by ;
no * i in INT by INT_1:def 2;
then no * i in INT \ by ;
then X1: [(mn * z),(no * i)] in [: the carrier of V,():] by ZFMISC_1:87;
set w = Class ((),[(mn * z),(no * i)]);
A7: Class ((),[(mn * z),(no * i)]) in Class () by ;
S1[q,A, Class ((),[(mn * z),(no * i)])]
proof
let mm, nn, ii be Integer; :: thesis: for mm being Element of INT.Ring
for z being Element of V st mm = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((),[z,ii]) holds
Class ((),[(mn * z),(no * i)]) = Class ((),[(mm * z),(nn * ii)])

let m1 be Element of INT.Ring; :: thesis: for z being Element of V st m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((),[z,ii]) holds
Class ((),[(mn * z),(no * i)]) = Class ((),[(m1 * z),(nn * ii)])

let zz be Element of V; :: thesis: ( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((),[zz,ii]) implies Class ((),[(mn * z),(no * i)]) = Class ((),[(m1 * zz),(nn * ii)]) )
assume A71: ( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((),[zz,ii]) ) ; :: thesis: Class ((),[(mn * z),(no * i)]) = Class ((),[(m1 * zz),(nn * ii)])
then A72: not ii in by TARSKI:def 1;
ii in INT by INT_1:def 2;
then ii in INT \ by ;
then X2: [zz,ii] in [: the carrier of V,():] by ZFMISC_1:87;
reconsider i2 = ii, n1 = nn as Element of INT.Ring by INT_1:def 2;
X51: [[zz,i2],[z,I]] in EQRZM V by ;
(n1 * i2) * (mn * z) = ((n1 * i2) * mn) * z by VECTSP_1:def 16
.= ((n1 * mn) * i2) * z
.= (n1 * mn) * (i2 * z) by VECTSP_1:def 16
.= (n1 * mn) * (I * zz) by
.= (no * m1) * (I * zz) by
.= ((no * m1) * I) * zz by VECTSP_1:def 16
.= ((no * I) * m1) * zz
.= (no * I) * (m1 * zz) by VECTSP_1:def 16 ;
then [[(mn * z),(no * I)],[(m1 * zz),(n1 * i2)]] in EQRZM V by ;
hence Class ((),[(mn * z),(no * i)]) = Class ((),[(m1 * zz),(nn * ii)]) by ; :: thesis: verum
end;
hence ex w being object st
( w in Class () & S1[q,A,w] ) by A7; :: thesis: verum
end;
consider f being Function of [:RAT,(Class ()):],(Class ()) such that
A14: for q, A being object st q in RAT & A in Class () holds
S1[q,A,f . (q,A)] from reconsider f = f as Function of [: the carrier of F_Rat,(Class ()):],(Class ()) ;
take f ; :: thesis: for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
f . (q,A) = Class ((),[(mm * z),(n * i)])

thus for q, A being object st q in RAT & A in Class () holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((),[z,i]) holds
f . (q,A) = Class ((),[(mm * z),(n * i)]) by A14; :: thesis: verum