let G be Group; :: thesis: for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).]
let H1, H2 be Subgroup of G; :: thesis: [.H1,H2.] is Subgroup of [.H1,((Omega). G).]
A1: H2 is Subgroup of (Omega). G by Lm2;
H1 is Subgroup of H1 by GROUP_2:54;
hence [.H1,H2.] is Subgroup of [.H1,((Omega). G).] by A1, GROUP_5:66; :: thesis: verum