let R be commutative domRing-like Ring; :: thesis: for Amp being AmpleSet of R st Amp is multiplicative holds
for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
let Amp be AmpleSet of R; :: thesis: ( Amp is multiplicative implies for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp )
assume A1: Amp is multiplicative ; :: thesis: for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
let x, y be Element of Amp; :: thesis: ( y divides x & y <> 0. R implies x / y in Amp )
assume A2: ( y divides x & y <> 0. R ) ; :: thesis: x / y in Amp

now

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

case A3: x <> 0. R ; :: thesis: x / y in Amp

set d = x / y;
A4: x = y * (x / y) by A2, Def4;
consider d' being Element of Amp such that
A5: d' is_associated_to x / y by Th22;
consider u being Element of R such that
A6: ( u is unital & (x / y) * u = d' ) by A5, Th18;
A7: u * x = y * d' by A4, A6, GROUP_1:def 4;
A8: y * d' in Amp by A1, Def10;
A9: x is_associated_to u * x

proof

x divides x ;
then A10: x divides u * x by Th7;
u divides 1. R by A6, Def2;
then consider e being Element of R such that
A11: u * e = 1. R by Def1;
(u * x) * e = (e * u) * x by GROUP_1:def 4
.= x by A11, VECTSP_1:def 19 ;
then u * x divides x by Def1;
hence x is_associated_to u * x by A10, Def3; :: thesis: verum

end;

(1. R) * x = x by VECTSP_1:def 19
.= u * x by A7, A8, A9, Th22 ;
then u = 1. R by A3, Th1;
then d' = x / y by A6, VECTSP_1:def 13;
hence x / y in Amp ; :: thesis: verum

end;

case A12: x = 0. R ; :: thesis: x / y in Amp

set d = x / y;
x = y * (x / y) by A2, Def4;
then A13: x / y = 0. R by A2, A12, VECTSP_2:def 5;
0. R is Element of Amp by Th24;
hence x / y in Amp by A13; :: thesis: verum

end;

end;

end;

hence x / y in Amp ; :: thesis: verum