let R be non empty multLoopStr ; :: thesis: for a, b being Element of R holds
( a divides a * b & ( R is commutative implies b divides a * b ) )
let a, b be Element of R; :: thesis: ( a divides a * b & ( R is commutative implies b divides a * b ) )
thus a divides a * b ; :: thesis: ( R is commutative implies b divides a * b )
assume A1: R is commutative ; :: thesis: b divides a * b
take a ; :: according to GCD_1:def 1 :: thesis: a * b = b * a
thus a * b = b * a by A1, GROUP_1:def 12; :: thesis: verum