consider P being strict Subgroup of G such that
A1: P is_Sylow_p-subgroup_of_prime p by Th12;
set P' = (Omega). P;
reconsider H' = (Omega). P as Element of Subgroups G by GROUP_3:def 1;
H' in the_sylow_p-subgroups_of_prime p,G by A1;
hence ( not the_sylow_p-subgroups_of_prime p,G is empty & the_sylow_p-subgroups_of_prime p,G is finite ) by FINSET_1:13, GROUP_3:19; :: thesis: verum