let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st c <> 0. R & c * a is_associated_to c * b holds
a is_associated_to b
let A, B, C be Element of R; :: thesis: ( C <> 0. R & C * A is_associated_to C * B implies A is_associated_to B )
assume that
A1: C <> 0. R and
A2: C * A is_associated_to C * B ; :: thesis: A is_associated_to B
C * B divides C * A by A2, Def3;
then A3: B divides A by A1, Th15;
C * A divides C * B by A2, Def3;
then A divides B by A1, Th15;
hence A is_associated_to B by A3, Def3; :: thesis: verum