let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds the carrier of (H * a) = ((- a) + H) + a
let a be Element of G; :: thesis: for H being Subgroup of G holds the carrier of (H * a) = ((- a) + H) + a
let H be Subgroup of G; :: thesis: the carrier of (H * a) = ((- a) + H) + a
thus the carrier of (H * a) = (carr H) * a by Def6A
.= ((- a) + H) + a by Th50 ; :: thesis: verum