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 A2: A is_associated_to B ; :: thesis: ex c being Element of R st
( c is unital & A * c = B )
then A divides B ;
then consider C being Element of R such that
A3: B = A * C ;
B divides A by A2;
then consider D being Element of R such that
A4: A = B * D ;

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

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 3;
then C * D = 1. R by A5, Th17;
then C is unital ;
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 )

1. R divides 1. R ;
then A7: 1. R is unital ;
B = 0. R by A3, A6;
then B = A * (1. R) by A6;
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 :: thesis: ( ex c being Element of R st
( c is unital & A * c = B ) & ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )

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 and
A9: A * C = B ;
C divides 1. R by A8;
then consider D being Element of R such that
A10: C * D = 1. R ;
A = A * (C * D) by A10
.= B * D by A9, GROUP_1:def 3 ;
then A11: B divides A ;
A divides B by A9;
hence ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) by A11; :: 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