theorem :: GAUSSINT:30

ex I being Function of Gauss_INT_Field,Gauss_RAT_Ring st
( ( for z being object st z in the carrier of Gauss_INT_Field holds
ex x, y being G_INTEG ex u being Element of Q. Gauss_INT_Ring st
( y <> 0 & u = [x,y] & z = QClass. u & I . z = x / y ) ) & I is one-to-one & I is onto & ( for x, y being Element of Gauss_INT_Field holds
( I . (x + y) = (I . x) + (I . y) & I . (x * y) = (I . x) * (I . y) ) ) & I . (0. Gauss_INT_Field) = 0. Gauss_RAT_Ring & I . (1. Gauss_INT_Field) = 1. Gauss_RAT_Ring )