let R be domRing; :: thesis: for c being non zero Element of R
for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds
b is_associated_to d
let c be non zero Element of R; :: thesis: for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds
b is_associated_to d
let b, a, d be Element of R; :: thesis: ( a * b is_associated_to c * d & a is_associated_to c implies b is_associated_to d )
assume AS: ( a * b is_associated_to c * d & a is_associated_to c ) ; :: thesis: b is_associated_to d
H0: c <> 0. R ;
consider u being Element of R such that
H1: ( u is unital & (a * b) * u = c * d ) by AS, GCD_1:18;
consider v being Element of R such that
H2: ( v is unital & c * v = a ) by AS, GCD_1:18;
H3: c * ((v * b) * u) = c * (v * (b * u)) by GROUP_1:def 3
.= (c * v) * (b * u) by GROUP_1:def 3
.= c * d by H1, H2, GROUP_1:def 3 ;
c is right_mult-cancelable by H0, ALGSTR_0:def 37;
then d = (v * b) * u by H3
.= (u * v) * b by GROUP_1:def 3 ;
hence b is_associated_to d by H1, H2, GCD_1:18; :: thesis: verum