MultGroup F is finite Subgroup of MultGroup F by GROUP_2:54;
hence MultGroup F is cyclic by GR_CY_3:38; :: thesis: verum