( ( for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i) ) & ( for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i) ) ) by LMP2, LMP2x;
hence ex b₁ being strict Subgroup of product F st the carrier of b₁ = ProjSet (F,i) by GROUP_2:61; :: thesis: verum