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

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

hence
F . i is normal Subgroup of gr UF
by GROUP_3:118; :: thesis: verum
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

end;for x being object st x in a * Fi holds

x in Fi * a

proof

hence
a * Fi c= Fi * a
; :: thesis: verum
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;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