let G be addGroup; :: thesis: for a, b being Element of G
for A being Subset of G holds (a * b) * A = a * (b + A)
let a, b be Element of G; :: thesis: for A being Subset of G holds (a * b) * A = a * (b + A)
let A be Subset of G; :: thesis: (a * b) * A = a * (b + A)
thus (a * b) * A = ({a} * {b}) * A by ThB37
.= a * (b + A) by Th35 ; :: thesis: verum