set X = Gauss_INT_Ring ;
for x, y being Element of Gauss_INT_Ring holds
( not x * y = 0. Gauss_INT_Ring or x = 0. Gauss_INT_Ring or y = 0. Gauss_INT_Ring )

proof

let x, y be Element of Gauss_INT_Ring; :: thesis: ( not x * y = 0. Gauss_INT_Ring or x = 0. Gauss_INT_Ring or y = 0. Gauss_INT_Ring )
reconsider xx = x, yy = y as Element of G_INT_SET ;
assume A1: x * y = 0. Gauss_INT_Ring ; :: thesis: ( x = 0. Gauss_INT_Ring or y = 0. Gauss_INT_Ring )
( xx is G_INTEG & yy is G_INTEG ) by Th2;
then xx * yy = 0 by A1, Th6;
hence ( x = 0. Gauss_INT_Ring or y = 0. Gauss_INT_Ring ) ; :: thesis: verum

end;

hence Gauss_INT_Ring is domRing-like by VECTSP_2:def 1; :: thesis: verum