let G be addGroup; :: thesis: for H being strict Subgroup of G holds H * (0_ G) = H
let H be strict Subgroup of G; :: thesis: H * (0_ G) = H
the carrier of (H * (0_ G)) = (carr H) * (0_ G) by Def6A
.= the carrier of H by ThB52 ;
hence H * (0_ G) = H by Th59; :: thesis: verum