let G be Group; :: thesis: for a being Element of
for A being Subset of
for H being Subgroup of G holds (A * H) * a = A * (H * a)
let a be Element of ; :: thesis: for A being Subset of
for H being Subgroup of G holds (A * H) * a = A * (H * a)
let A be Subset of ; :: thesis: for H being Subgroup of G holds (A * H) * a = A * (H * a)
let H be Subgroup of G; :: thesis: (A * H) * a = A * (H * a)
thus (A * H) * a = A * (H * {a}) by GROUP_2:117
.= A * (H * a) ; :: thesis: verum