let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st a <> 0. R & a * b divides a * c holds
b divides c
let A, B, C be Element of R; :: thesis: ( A <> 0. R & A * B divides A * C implies B divides C )
assume that
A1: A <> 0. R and
A2: A * B divides A * C ; :: thesis: B divides C
consider D being Element of R such that
A3: (A * B) * D = A * C by A2;
A divides A * C ;
then A4: (A * C) / A = (A / A) * C by A1, Th11;
A divides A * (B * D) ;
then A5: (A * (B * D)) / A = (A / A) * (B * D) by A1, Th11;
A6: A * (B * D) = A * C by A3, GROUP_1:def 3;
B * D = (1. R) * (B * D)
.= (A / A) * C by A1, A6, A5, A4, Th9
.= (1. R) * C by A1, Th9
.= C ;
hence B divides C ; :: thesis: verum