let G be addGroup; :: thesis: for a, b being Element of G
for H being Subgroup of G holds (H * a) * b = H * (a + b)
let a, b be Element of G; :: thesis: for H being Subgroup of G holds (H * a) * b = H * (a + b)
let H be Subgroup of G; :: thesis: (H * a) * b = H * (a + b)
the carrier of ((H * a) * b) = (carr (H * a)) * b by Def6A
.= ((carr H) * a) * b by Def6A
.= (carr H) * (a + b) by Th47
.= the carrier of (H * (a + b)) by Def6A ;
hence (H * a) * b = H * (a + b) by Th59; :: thesis: verum