consider H1 being strict Subgroup of G such that
A1: the carrier of H1 = ((- a) + H) + (- (- a)) by Th127;
the carrier of H1 = (carr H) * a by A1, Th50;
hence ex b₁ being strict Subgroup of G st the carrier of b₁ = (carr H) * a ; :: thesis: verum