let G be Group; :: thesis: for H being Subgroup of G holds (carr H) * (carr H) = carr H
let H be Subgroup of G; :: thesis: (carr H) * (carr H) = carr H
A1: for g being Element of G st g in carr H holds
g " in carr H by Th75;
for g1, g2 being Element of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H by Th74;
hence (carr H) * (carr H) = carr H by A1, Th22; :: thesis: verum