theorem :: GRNILP_1:14

for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).]