let G be Group; :: thesis: for H being Subgroup of G holds 1_ H = 1_ G
let H be Subgroup of G; :: thesis: 1_ H = 1_ G
consider h being Element of H;
reconsider g = h, g9 = 1_ H as Element of G by Th51;
h * (1_ H) = h by GROUP_1:def 5;
then g * g9 = g by Th52;
hence 1_ H = 1_ G by GROUP_1:15; :: thesis: verum