let R be non empty add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for a, b being Element of R
for n being Element of NAT holds (a * n) * b = a * (n * b)
let a, b be Element of R; :: thesis: for n being Element of NAT holds (a * n) * b = a * (n * b)
let n be Element of NAT ; :: thesis: (a * n) * b = a * (n * b)
thus (a * n) * b = (n * a) * b by Th17
.= n * (a * b) by Th19
.= (a * b) * n by Th17
.= a * (n * b) by Th20 ; :: thesis: verum