( ( 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 Th5, Th6;
hence ex b₁ being strict Subgroup of product F st the carrier of b₁ = ProjSet (F,i) by GROUP_2:52; :: thesis: verum