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 A1: ( A <> 0. R & A * B divides A * C ) ; :: thesis: B divides C
then consider D being Element of R such that
A2: (A * B) * D = A * C by Def1;
A3: A * (B * D) = A * C by A2, GROUP_1:def 4;
A4: (A * (B * D)) / A = (A / A) * (B * D)

proof

A divides A * (B * D) by Th6;
hence (A * (B * D)) / A = (A / A) * (B * D) by A1, Th11; :: thesis: verum

end;

A5: (A * C) / A = (A / A) * C

proof

A divides A * C by Th6;
hence (A * C) / A = (A / A) * C by A1, Th11; :: thesis: verum

end;

B * D = (1. R) * (B * D) by VECTSP_1:def 19
.= (A / A) * C by A1, A3, A4, A5, Th9
.= (1. R) * C by A1, Th9
.= C by VECTSP_1:def 19 ;
hence B divides C by Def1; :: thesis: verum