let I be non empty set ; for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds
sum F1 is Subgroup of sum F2
let F1, F2 be Group-Family of I; ( ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) implies sum F1 is Subgroup of sum F2 )
assume A1:
for i being Element of I holds F1 . i is Subgroup of F2 . i
; sum F1 is Subgroup of sum F2
for x being object st x in [#] (sum F1) holds
x in [#] (sum F2)
then A5:
[#] (sum F1) c= [#] (sum F2)
;
set mp1 = the multF of (product F1);
set mp2 = the multF of (product F2);
set ms1 = the multF of (sum F1);
set ms2 = the multF of (sum F2);
set cp1 = [#] (product F1);
set cp2 = [#] (product F2);
set cs1 = [#] (sum F1);
set cs2 = [#] (sum F2);
[#] (sum F1) c= [#] (product F1)
by GROUP_2:def 5;
then A6:
[:([#] (sum F1)),([#] (sum F1)):] c= [:([#] (product F1)),([#] (product F1)):]
by ZFMISC_1:96;
A7:
[:([#] (sum F1)),([#] (sum F1)):] c= [:([#] (sum F2)),([#] (sum F2)):]
by A5, ZFMISC_1:96;
A8:
product F1 is Subgroup of product F2
by A1, Th20;
the multF of (sum F1) =
the multF of (product F1) || ([#] (sum F1))
by GROUP_2:def 5
.=
( the multF of (product F2) || ([#] (product F1))) || ([#] (sum F1))
by A8, GROUP_2:def 5
.=
the multF of (product F2) || ([#] (sum F1))
by A6, FUNCT_1:51
.=
( the multF of (product F2) || ([#] (sum F2))) || ([#] (sum F1))
by A7, FUNCT_1:51
.=
the multF of (sum F2) || ([#] (sum F1))
by GROUP_2:def 5
;
hence
sum F1 is Subgroup of sum F2
by A5, GROUP_2:def 5; verum