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