let x, y, z be G_INTEG; :: thesis: ( x is_associated_to y & y is_associated_to z implies x is_associated_to z )
assume A1: ( x is_associated_to y & y is_associated_to z ) ; :: thesis: x is_associated_to z
consider c being G_INTEG such that
A2: ( c is g_int_unit & x = c * y ) by A1, Th40;
consider d being G_INTEG such that
A3: ( d is g_int_unit & y = d * z ) by A1, Th40;
A4: x = (c * d) * z by A2, A3;
reconsider e = c * d as G_INTEG ;
Norm e = 1 * (Norm d) by A2, Th34
.= 1 by A3 ;
hence x is_associated_to z by A4, Def20, Th40; :: thesis: verum