let R be commutative domRing-like Ring; :: thesis: for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) )
A1: for a, b being Element of R st a is_associated_to b holds
ex c being Element of R st
( c is unital & a * c = b )

proof

let A, B be Element of R; :: thesis: ( A is_associated_to B implies ex c being Element of R st
( c is unital & A * c = B ) )
assume A is_associated_to B ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )
then A2: ( A divides B & B divides A ) by Def3;
then consider C being Element of R such that
A3: B = A * C by Def1;
consider D being Element of R such that
A4: A = B * D by A2, Def1;

now

per cases ( A <> 0. R or A = 0. R ) ;

case A5: A <> 0. R ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )

A = A * (C * D) by A3, A4, GROUP_1:def 4;
then C * D = 1. R by A5, Th17;
then C divides 1. R by Def1;
then C is unital by Def2;
hence ex c being Element of R st
( c is unital & A * c = B ) by A3; :: thesis: verum

end;

case A6: A = 0. R ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )

then B = 0. R by A3, VECTSP_1:39;
then A7: B = A * (1. R) by A6, VECTSP_1:def 13;
1. R is unital

proof

thus 1. R divides 1. R ; :: according to GCD_1:def 2 :: thesis: verum

end;

hence ex c being Element of R st
( c is unital & A * c = B ) by A7; :: thesis: verum

end;

end;

end;

hence ex c being Element of R st
( c is unital & A * c = B ) ; :: thesis: verum

end;

for a, b being Element of R st ex c being Element of R st
( c is unital & a * c = b ) holds
a is_associated_to b

proof

let A, B be Element of R; :: thesis: ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )

proof

now

assume ex c being Element of R st
( c is unital & A * c = B ) ; :: thesis: ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
then consider C being Element of R such that
A8: ( C is unital & A * C = B ) ;
C divides 1. R by A8, Def2;
then consider D being Element of R such that
A9: C * D = 1. R by Def1;
A = A * (C * D) by A9, VECTSP_1:def 13
.= B * D by A8, GROUP_1:def 4 ;
then A10: B divides A by Def1;
A divides B by A8, Def1;
hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) by A10, Def3; :: thesis: verum

end;

hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) ; :: thesis: verum

end;

hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) ; :: thesis: verum

end;

hence for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) ) by A1; :: thesis: verum