let R be commutative domRing-like Ring; :: thesis: for a, b being Element of R st b divides a & b <> 0. R holds
( a / b = 0. R iff a = 0. R )
let a, b be Element of R; :: thesis: ( b divides a & b <> 0. R implies ( a / b = 0. R iff a = 0. R ) )
assume that
A1: b divides a and
A2: b <> 0. R ; :: thesis: ( a / b = 0. R iff a = 0. R )
hereby :: thesis: ( a = 0. R implies a / b = 0. R )
assume a / b = 0. R ; :: thesis: a = 0. R
then a = (0. R) * b by A1, A2, Def4
.= 0. R ;
hence a = 0. R ; :: thesis: verum
end;
assume a = 0. R ; :: thesis: a / b = 0. R
then 0. R = (a / b) * b by A1, A2, Def4;
hence a / b = 0. R by A2, VECTSP_2:def 1; :: thesis: verum