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

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