let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st c <> 0. R & c divides a & c divides b holds
( a / c = b / c iff a = b )
let a, b, c be Element of R; :: thesis: ( c <> 0. R & c divides a & c divides b implies ( a / c = b / c iff a = b ) )
assume A1: c <> 0. R ; :: thesis: ( not c divides a or not c divides b or ( a / c = b / c iff a = b ) )
assume that
A2: c divides a and
A3: c divides b ; :: thesis: ( a / c = b / c iff a = b )
now :: thesis: ( a / c = b / c & a / c = b / c implies a = b )
assume a / c = b / c ; :: thesis: ( a / c = b / c implies a = b )
consider e being Element of R such that
A4: e = b / c ;
e * c = b by A1, A3, A4, Def4;
hence ( a / c = b / c implies a = b ) by A1, A2, A4, Def4; :: thesis: verum
end;
hence ( a / c = b / c iff a = b ) ; :: thesis: verum