let x, y be G_INTEG; :: thesis: ( x is_associated_to y iff ex c being G_INTEG st
( c is g_int_unit & x = c * y ) )

hereby :: thesis: ( ex c being G_INTEG st
( c is g_int_unit & x = c * y ) implies x is_associated_to y )

assume A1: x is_associated_to y ; :: thesis: ex c being G_INTEG st
( c is g_int_unit & x = c * y )
reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by Th3;
consider c1 being Element of Gauss_INT_Ring such that
A2: ( c1 is unital & y1 * c1 = x1 ) by A1, Th38, GCD_1:18;
reconsider c = c1 as G_INTEG by Th2;
A3: c is g_int_unit by A2, Th39;
c1 * y1 = c * y by Th6;
hence ex c being G_INTEG st
( c is g_int_unit & x = c * y ) by A2, A3; :: thesis: verum

end;

given c0 being G_INTEG such that A4: ( c0 is g_int_unit & x = c0 * y ) ; :: thesis: x is_associated_to y
reconsider xx = x as Element of Gauss_INT_Ring by Th3;
reconsider yy = y as Element of Gauss_INT_Ring by Th3;
reconsider c = c0 as Element of Gauss_INT_Ring by Th3;
A5: c is unital by A4, Th39;
c * yy = c0 * y by Th6;
hence x is_associated_to y by A4, A5, Th37, GCD_1:18; :: thesis: verum