defpred S₁[ object , object ] means ex x, y being G_INTEG ex u being Element of Q. Gauss_INT_Ring st
( y <> 0 & u = [x,y] & $1 = QClass. u & $2 = x / y );
A1: for z being object st z in the carrier of Gauss_INT_Field holds
ex w being object st
( w in the carrier of Gauss_RAT_Ring & S₁[z,w] )

proof

let z be object ; :: thesis:
assume z in the carrier of Gauss_INT_Field ; :: thesis:
then consider u being Element of Q. Gauss_INT_Ring such that
A2: z = QClass. u by QUOFIELD:def 5;
consider x1, y1 being Element of Gauss_INT_Ring such that
A3: ( u = [x1,y1] & y1 <> 0. Gauss_INT_Ring ) by QUOFIELD:def 1;
reconsider x = x1, y = y1 as G_INTEG by Th2;
take x / y ; :: thesis:
thus ( x / y in the carrier of Gauss_RAT_Ring & S₁[z,x / y] ) by A2, A3; :: thesis:

end;

consider I being Function of Gauss_INT_Field,Gauss_RAT_Ring such that
A4: for z being object st z in the carrier of Gauss_INT_Field holds
S₁[z,I . z] from FUNCT_2:sch 1(A1);

A5: now :: thesis:

let z1, z2 be object ; :: thesis:
assume A6: ( z1 in dom I & z2 in dom I & I . z1 = I . z2 ) ; :: thesis:
then A7: ( z1 in the carrier of Gauss_INT_Field & z2 in the carrier of Gauss_INT_Field ) by FUNCT_2:def 1;
then consider x1, y1 being G_INTEG, u1 being Element of Q. Gauss_INT_Ring such that
A8: ( y1 <> 0 & u1 = [x1,y1] & z1 = QClass. u1 & I . z1 = x1 / y1 ) by A4;
consider x2, y2 being G_INTEG, u2 being Element of Q. Gauss_INT_Ring such that
A9: ( y2 <> 0 & u2 = [x2,y2] & z2 = QClass. u2 & I . z2 = x2 / y2 ) by A4, A7;
thus z1 = z2 by A6, A8, A9, Lm5; :: thesis:

end;

then A10: I is one-to-one by FUNCT_1:def 4;

now :: thesis:

let p1 be object ; :: thesis:
assume p1 in the carrier of Gauss_RAT_Ring ; :: thesis:
then reconsider p = p1 as G_RAT by Th10;
consider x, y being G_INTEG such that
A11: ( y <> 0 & p = x / y ) by Th12;
reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by Th3;
y1 <> 0. Gauss_INT_Ring by A11;
then reconsider u1 = [x1,y1] as Element of Q. Gauss_INT_Ring by QUOFIELD:def 1;
set z1 = QClass. u1;
consider x2, y2 being G_INTEG, u2 being Element of Q. Gauss_INT_Ring such that
A12: ( y2 <> 0 & u2 = [x2,y2] & QClass. u1 = QClass. u2 & I . (QClass. u1) = x2 / y2 ) by A4;
x / y = x2 / y2 by Lm5, A12, A11;
hence ex z1 being object st
( z1 in the carrier of Gauss_INT_Field & I . z1 = p1 ) by A12, A11; :: thesis:

end;

then rng I = the carrier of Gauss_RAT_Ring by FUNCT_2:10;
then A13: I is onto by FUNCT_2:def 3;
A14: for z1, z2 being Element of Gauss_INT_Field holds
( I . (z1 + z2) = (I . z1) + (I . z2) & I . (z1 * z2) = (I . z1) * (I . z2) )

proof

let z1, z2 be Element of Gauss_INT_Field; :: thesis:
consider x1, y1 being G_INTEG, u1 being Element of Q. Gauss_INT_Ring such that
A15: ( y1 <> 0 & u1 = [x1,y1] & z1 = QClass. u1 & I . z1 = x1 / y1 ) by A4;
consider x2, y2 being G_INTEG, u2 being Element of Q. Gauss_INT_Ring such that
A16: ( y2 <> 0 & u2 = [x2,y2] & z2 = QClass. u2 & I . z2 = x2 / y2 ) by A4;
set z12 = z1 + z2;
consider x12, y12 being G_INTEG, u12 being Element of Q. Gauss_INT_Ring such that
A17: ( y12 <> 0 & u12 = [x12,y12] & z1 + z2 = QClass. u12 & I . (z1 + z2) = x12 / y12 ) by A4;
A18: (x1 / y1) + (x2 / y2) = ((x1 * y2) + (x2 * y1)) / (y1 * y2) by A15, A16, XCMPLX_1:116;
A19: ( (u1 `1) * (u2 `2) = x1 * y2 & (u2 `1) * (u1 `2) = x2 * y1 & (u1 `2) * (u2 `2) = y1 * y2 ) by Th6, A15, A16;
A20: padd (u1,u2) = [((x1 * y2) + (x2 * y1)),(y1 * y2)] by A19, Th4;
z1 + z2 = qadd ((QClass. u1),(QClass. u2)) by A15, A16, QUOFIELD:def 12
.= QClass. (padd (u1,u2)) by QUOFIELD:9 ;
then A21: u12 in QClass. (padd (u1,u2)) by A17, QUOFIELD:5;
A22: (u12 `1) * ((padd (u1,u2)) `2) = x12 * (y1 * y2) by Th6, A17, A19;
((padd (u1,u2)) `1) * (u12 `2) = ((x1 * y2) + (y1 * x2)) * y12 by Th6, A17, A20;
then x12 * (y1 * y2) = ((x1 * y2) + (y1 * x2)) * y12 by A22, A21, QUOFIELD:def 4;
then A23: x12 / y12 = ((x1 * y2) + (x2 * y1)) / (y1 * y2) by A15, A16, A17, XCMPLX_1:94;
set z12 = z1 * z2;
consider x12, y12 being G_INTEG, u12 being Element of Q. Gauss_INT_Ring such that
A24: ( y12 <> 0 & u12 = [x12,y12] & z1 * z2 = QClass. u12 & I . (z1 * z2) = x12 / y12 ) by A4;
A25: (x1 / y1) * (x2 / y2) = (x1 * x2) / (y1 * y2) by XCMPLX_1:76;
A26: ( (u1 `1) * (u2 `1) = x1 * x2 & (u2 `2) * (u1 `2) = y1 * y2 ) by Th6, A15, A16;
z1 * z2 = qmult ((QClass. u1),(QClass. u2)) by A15, A16, QUOFIELD:def 13
.= QClass. (pmult (u1,u2)) by QUOFIELD:10 ;
then A27: u12 in QClass. (pmult (u1,u2)) by A24, QUOFIELD:5;
A28: (u12 `1) * ((pmult (u1,u2)) `2) = x12 * (y1 * y2) by Th6, A24, A26;
((pmult (u1,u2)) `1) * (u12 `2) = (x1 * x2) * y12 by Th6, A24, A26;
then x12 * (y1 * y2) = (x1 * x2) * y12 by A28, A27, QUOFIELD:def 4;
then x12 / y12 = (x1 * x2) / (y1 * y2) by A15, A16, A24, XCMPLX_1:94;
hence ( I . (z1 + z2) = (I . z1) + (I . z2) & I . (z1 * z2) = (I . z1) * (I . z2) ) by A23, A25, A18, A24, A17, A15, A16, Th27, Th29; :: thesis:

end;