let I be non empty set ; :: thesis: for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for i being Element of I holds F . i is normal Subgroup of gr UF
let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for i being Element of I holds F . i is normal Subgroup of gr UF
let F be component-commutative Subgroup-Family of I,G; :: thesis: for UF being Subset of G st UF = Union (Carrier F) holds
for i being Element of I holds F . i is normal Subgroup of gr UF
let UF be Subset of G; :: thesis: ( UF = Union (Carrier F) implies for i being Element of I holds F . i is normal Subgroup of gr UF )
assume A1: UF = Union (Carrier F) ; :: thesis: for i being Element of I holds F . i is normal Subgroup of gr UF
let i be Element of I; :: thesis: F . i is normal Subgroup of gr UF
A2: dom (Carrier F) = I by PARTFUN1:def 2;
A3: F . i is Subgroup of G by Def1;
(Carrier F) . i in rng (Carrier F) by A2, FUNCT_1:3;
then [#] (F . i) in rng (Carrier F) by PENCIL_3:7;
then [#] (F . i) c= union (rng (Carrier F)) by ZFMISC_1:74;
then A4: [#] (F . i) c= UF by A1, CARD_3:def 4;
UF c= [#] (gr UF) by GROUP_4:def 4;
then [#] (F . i) c= [#] (gr UF) by A4;
then reconsider Fi = F . i as Subgroup of gr UF by A3, GROUP_2:57;
for a being Element of (gr UF) holds a * Fi c= Fi * a

proof

let a be Element of (gr UF); :: thesis: a * Fi c= Fi * a
for x being object st x in a * Fi holds
x in Fi * a

proof

let x be object ; :: thesis: ( x in a * Fi implies x in Fi * a )
assume x in a * Fi ; :: thesis: x in Fi * a
then consider g being Element of (gr UF) such that
A5: ( x = a * g & g in Fi ) by GROUP_2:103;
reconsider a1 = a as Element of G by GROUP_2:42;
a1 in gr UF ;
then consider h being finite-support Function of I,(gr UF) such that
A6: ( h in sum F & a = Product h ) by A1, Th13;
reconsider m = h . i as Element of (gr UF) ;
A7: h in product F by A6, GROUP_2:40;
A8: h . i in F . i by A6, GROUP_19:5, GROUP_2:40;
reconsider I0 = I \ {i} as Subset of I ;
1_ (F . i) in gr UF by A3, GROUP_2:47;
then reconsider h0 = h +* (i,(1_ (F . i))) as finite-support Function of I,(gr UF) by GROUP_19:26;
A9: h0 in product F by A6, GROUP_19:24, GROUP_2:40;
dom h = I by FUNCT_2:def 1;
then A10: h0 . i = 1_ (F . i) by FUNCT_7:31;
A11: a * g = ((Product h0) * m) * g by A6, A7, Th9
.= (Product h0) * (m * g) by GROUP_1:def 3 ;
A12: a * g = (m * g) * (Product h0) by A5, A8, A9, A10, A11, GROUP_2:50, Th10
.= ((m * g) * (1_ (gr UF))) * (Product h0) by GROUP_1:def 4
.= ((m * g) * ((m ") * m)) * (Product h0) by GROUP_1:def 5
.= (((m * g) * (m ")) * m) * (Product h0) by GROUP_1:def 3
.= ((m * g) * (m ")) * (m * (Product h0)) by GROUP_1:def 3
.= ((m * g) * (m ")) * ((Product h0) * m) by A7, Th9
.= ((m * g) * (m ")) * a by A6, A7, Th9 ;
m " in Fi by A8, GROUP_2:51;
then g * (m ") in Fi by A5, GROUP_2:50;
then m * (g * (m ")) in Fi by A8, GROUP_2:50;
then (m * g) * (m ") in Fi by GROUP_1:def 3;
hence x in Fi * a by A5, A12, GROUP_2:104; :: thesis: verum

end;

hence a * Fi c= Fi * a ; :: thesis: verum

end;

hence F . i is normal Subgroup of gr UF by GROUP_3:118; :: thesis: verum