theorem
Th33
:
:: GROUP_19:33
for
I
being non
empty
set
for
F
being
Group-Family
of
I
for
i
being
Element
of
I
holds
ProjGroup
(
F
,
i
) is
Subgroup
of
sum
F