let I be non empty set ; :: thesis: for F being Group-Family of I
for i being Element of I holds ProjGroup (F,i) is Subgroup of sum F
let F be Group-Family of I; :: thesis: for i being Element of I holds ProjGroup (F,i) is Subgroup of sum F
let i be Element of I; :: thesis: ProjGroup (F,i) is Subgroup of sum F
set S = ProjGroup (F,i);
set G = sum F;
for x being object st x in [#] (ProjGroup (F,i)) holds
x in [#] (sum F)

proof

let x be object ; :: thesis: ( x in [#] (ProjGroup (F,i)) implies x in [#] (sum F) )
assume A1: x in [#] (ProjGroup (F,i)) ; :: thesis: x in [#] (sum F)
then x in ProjGroup (F,i) ;
then x in product F by GROUP_2:40;
then reconsider x = x as Element of (product F) ;
x in ProjSet (F,i) by A1, GROUP_12:def 2;
then consider h being Element of (F . i) such that
A3: x = (1_ (product F)) +* (i,h) by GROUP_12:def 1;
support (x,F) c= {i} by A3, Th17;
then x in sum F by Th8;
hence x in [#] (sum F) ; :: thesis: verum

end;

then A14: [#] (ProjGroup (F,i)) c= [#] (sum F) ;
A16: the multF of (sum F) = the multF of (product F) || the carrier of (sum F) by GROUP_2:def 5
.= the multF of (product F) | [:([#] (sum F)),([#] (sum F)):] by REALSET1:def 2 ;
the multF of (sum F) || ([#] (ProjGroup (F,i))) = ( the multF of (product F) | [:([#] (sum F)),([#] (sum F)):]) | [:([#] (ProjGroup (F,i))),([#] (ProjGroup (F,i))):] by A16, REALSET1:def 2
.= the multF of (product F) | [:([#] (ProjGroup (F,i))),([#] (ProjGroup (F,i))):] by A14, RELAT_1:74, ZFMISC_1:96
.= the multF of (product F) || ([#] (ProjGroup (F,i))) by REALSET1:def 2
.= the multF of (ProjGroup (F,i)) by GROUP_2:def 5 ;
hence ProjGroup (F,i) is Subgroup of sum F by A14, GROUP_2:def 5; :: thesis: verum