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
set h = the Element of H;
reconsider g = the Element of H, g9 = 1_ H as Element of G by Th42;
the Element of H * (1_ H) = the Element of H by GROUP_1:def 4;
then g * g9 = g by Th43;
hence 1_ H = 1_ G by GROUP_1:7; :: thesis: verum