let R be non empty associative multLoopStr ; :: thesis: for a, b, c being Element of R st a divides b holds
c * a divides c * b
let A, B, C be Element of R; :: thesis: ( A divides B implies C * A divides C * B )
assume A divides B ; :: thesis: C * A divides C * B
then consider D being Element of R such that
A1: A * D = B ;
(C * A) * D = C * B by A1, GROUP_1:def 3;
hence C * A divides C * B ; :: thesis: verum