let I be non empty set ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: sum F1 is Subgroup of sum F2
for x being object st x in [#] (sum F1) holds
x in [#] (sum F2)
proof
let x be object ; :: thesis: ( x in [#] (sum F1) implies x in [#] (sum F2) )
assume A2: x in [#] (sum F1) ; :: thesis: x in [#] (sum F2)
then x in sum F1 ;
then x in product F1 by GROUP_2:40;
then reconsider x = x as Element of (product F1) ;
product F1 is Subgroup of product F2 by A1, Th20;
then reconsider y = x as Element of (product F2) by GROUP_2:42;
for i being object st i in support (y,F2) holds
i in support (x,F1)
proof
let i be object ; :: thesis: ( i in support (y,F2) implies i in support (x,F1) )
assume i in support (y,F2) ; :: thesis: i in support (x,F1)
then consider Z being Group such that
A4: ( Z = F2 . i & y . i <> 1_ Z & i in I ) by GROUP_19:def 1;
reconsider i = i as Element of I by A4;
F1 . i is Subgroup of F2 . i by A1;
then ( x . i <> 1_ (F1 . i) & i in I ) by A4, GROUP_2:44;
hence i in support (x,F1) by GROUP_19:def 1; :: thesis: verum
end;
then support (y,F2) c= support (x,F1) ;
then y in sum F2 by A2, GROUP_19:8;
hence x in [#] (sum F2) ; :: thesis: verum
end;
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; :: thesis: verum