let G be Group; :: thesis: for H being strict Subgroup of G
for g1, g2 being Element of G st g1 in (carr G) . H & g2 in (carr G) . H holds
g1 * g2 in (carr G) . H
let H be strict Subgroup of G; :: thesis: for g1, g2 being Element of G st g1 in (carr G) . H & g2 in (carr G) . H holds
g1 * g2 in (carr G) . H
let g1, g2 be Element of G; :: thesis: ( g1 in (carr G) . H & g2 in (carr G) . H implies g1 * g2 in (carr G) . H )
assume ( g1 in (carr G) . H & g2 in (carr G) . H ) ; :: thesis: g1 * g2 in (carr G) . H
then ( g1 in H & g2 in H ) by Th18;
then g1 * g2 in H by GROUP_2:50;
hence g1 * g2 in (carr G) . H by Th18; :: thesis: verum