let R be non empty associative commutative multLoopStr ; :: thesis: for a, b, c, d being Element of R st b divides a & d divides c holds
b * d divides a * c
let a, b, c, d be Element of R; :: thesis: ( b divides a & d divides c implies b * d divides a * c )
assume that
A1: b divides a and
A2: d divides c ; :: thesis: b * d divides a * c
consider x being Element of R such that
A3: b * x = a by A1, Def1;
consider y being Element of R such that
A4: d * y = c by A2, Def1;
(b * d) * (y * x) = ((b * d) * y) * x by GROUP_1:def 3
.= (b * c) * x by A4, GROUP_1:def 3
.= a * c by A3, GROUP_1:def 3 ;
hence b * d divides a * c by Def1; :: thesis: verum