let a, b be Element of Gauss_INT_Ring; :: thesis: for aa, bb being G_INTEG st a = aa & b = bb & a is_associated_to b holds
aa is_associated_to bb
let aa, bb be G_INTEG; :: thesis: ( a = aa & b = bb & a is_associated_to b implies aa is_associated_to bb )
assume A1: ( a = aa & b = bb ) ; :: thesis: ( not a is_associated_to b or aa is_associated_to bb )
assume a is_associated_to b ; :: thesis: aa is_associated_to bb
then A2: ( a divides b & b divides a ) by GCD_1:def 3;
then consider ca being Element of Gauss_INT_Ring such that
A3: b = a * ca by GCD_1:def 1;
consider cb being Element of Gauss_INT_Ring such that
A4: a = b * cb by A2, GCD_1:def 1;
reconsider cca = ca as G_INTEG by Th2;
reconsider ccb = cb as G_INTEG by Th2;
bb = aa * cca by A1, A3, Th6;
then A5: aa Divides bb ;
aa = bb * ccb by A1, A4, Th6;
then bb Divides aa ;
hence aa is_associated_to bb by A5; :: thesis: verum