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 () 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 () 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 () 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 () implies for i being Element of I holds F . i is normal Subgroup of gr UF )
assume A1: UF = Union () ; :: 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 () = I by PARTFUN1:def 2;
A3: F . i is Subgroup of G by Def1;
(Carrier F) . i in rng () by ;
then [#] (F . i) in rng () by PENCIL_3:7;
then [#] (F . i) c= union (rng ()) by ZFMISC_1:74;
then A4: [#] (F . i) c= UF by ;
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 ;
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 ;
reconsider m = h . i as Element of (gr UF) ;
A7: h in product F by ;
A8: h . i in F . i by ;
reconsider I0 = I \ {i} as Subset of I ;
1_ (F . i) in gr UF by ;
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 ;
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
.= ((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
.= ((m * g) * (m ")) * a by A6, A7, Th9 ;
m " in Fi by ;
then g * (m ") in Fi by ;
then m * (g * (m ")) in Fi by ;
then (m * g) * (m ") in Fi by GROUP_1:def 3;
hence x in Fi * a by ; :: 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