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