let O be set ; :: thesis: for G being GroupWithOperators of O

for H1 being StableSubgroup of G holds 1_ G = 1_ H1

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds 1_ G = 1_ H1

let H1 be StableSubgroup of G; :: thesis: 1_ G = 1_ H1

reconsider H19 = H1 as Subgroup of G by Def7;

1_ H1 = 1_ H19 ;

hence 1_ G = 1_ H1 by GROUP_2:44; :: thesis: verum

for H1 being StableSubgroup of G holds 1_ G = 1_ H1

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds 1_ G = 1_ H1

let H1 be StableSubgroup of G; :: thesis: 1_ G = 1_ H1

reconsider H19 = H1 as Subgroup of G by Def7;

1_ H1 = 1_ H19 ;

hence 1_ G = 1_ H1 by GROUP_2:44; :: thesis: verum