let x, y be G_INTEG; :: thesis: ( x is_associated_to y implies x *' is_associated_to y *' )
assume x is_associated_to y ; :: thesis: x *' is_associated_to y *'
then consider c being G_INTEG such that
A1: ( c is g_int_unit & x = c * y ) by Th40;
A2: x *' = (c *') * (y *') by A1, COMPLEX1:35;
Norm (c *') = 1 by A1;
hence x *' is_associated_to y *' by A2, Def20, Th40; :: thesis: verum