let I be non empty set ; :: thesis: for F, Z being Group-Family of I st ( for i being Element of I holds Z . i = center (F . i) ) holds
center (product F) = product Z
let F, Z be Group-Family of I; :: thesis: ( ( for i being Element of I holds Z . i = center (F . i) ) implies center (product F) = product Z )
assume A1: for i being Element of I holds Z . i = center (F . i) ; :: thesis: center (product F) = product Z
A2: for a being Element of (product F) holds
( a in product Z iff for b being Element of (product F) holds a * b = b * a )

proof

let a be Element of (product F); :: thesis: ( a in product Z iff for b being Element of (product F) holds a * b = b * a )
thus ( a in product Z implies for b being Element of (product F) holds a * b = b * a ) :: thesis: ( ( for b being Element of (product F) holds a * b = b * a ) implies a in product Z )

proof

assume B1: a in product Z ; :: thesis: for b being Element of (product F) holds a * b = b * a
let b be Element of (product F); :: thesis: a * b = b * a
reconsider ab = a * b, ba = b * a as Element of (product F) ;
( ab in product F & ba in product F ) ;
then ( ab in product (Carrier F) & ba in product (Carrier F) ) by GROUP_7:def 2;
then B3: ( dom ab = I & dom ba = I ) by PARTFUN1:def 2;
for i being Element of I holds (a * b) . i = (b * a) . i

proof

let i be Element of I; :: thesis: (a * b) . i = (b * a) . i
a . i in Z . i by B1, GROUP_19:5;
then C1: a . i in center (F . i) by A1;
(a * b) . i = (a /. i) * (b /. i) by GROUP_7:1
.= (b /. i) * (a /. i) by C1, GROUP_5:77
.= (b * a) . i by GROUP_7:1 ;
hence (a * b) . i = (b * a) . i ; :: thesis: verum

end;

hence a * b = b * a by B3; :: thesis: verum

end;

thus ( ( for b being Element of (product F) holds a * b = b * a ) implies a in product Z ) :: thesis: verum

proof

assume B1: for b being Element of (product F) holds a * b = b * a ; :: thesis: a in product Z
B2: for i being Element of I holds a . i in Z . i

proof

let i be Element of I; :: thesis: a . i in Z . i
C1: for b being Element of (product F) holds (a /. i) * (b /. i) = (b /. i) * (a /. i)

proof

let b be Element of (product F); :: thesis: (a /. i) * (b /. i) = (b /. i) * (a /. i)
( (a * b) . i = (a /. i) * (b /. i) & (b * a) . i = (b /. i) * (a /. i) ) by GROUP_7:1;
hence (a /. i) * (b /. i) = (b /. i) * (a /. i) by B1; :: thesis: verum

end;

for bi being Element of (F . i) holds (a /. i) * bi = bi * (a /. i)

proof

let bi be Element of (F . i); :: thesis: (a /. i) * bi = bi * (a /. i)
reconsider b = (1ProdHom (F,i)) . bi as Element of (product F) by GROUP_2:42;
D1: dom (1_ (product F)) = I by GROUP_19:3;
b = (1_ (product F)) +* (i,bi) by GROUP_12:def 3;
then b /. i = bi by D1, FUNCT_7:31;
hence (a /. i) * bi = bi * (a /. i) by C1; :: thesis: verum

end;

then a . i in center (F . i) by GROUP_5:77;
hence a . i in Z . i by A1; :: thesis: verum

end;

a in product F ;
then a in product (Carrier F) by GROUP_7:def 2;
then dom a = I by PARTFUN1:def 2;
hence a in product Z by B2, Th47; :: thesis: verum

end;

end;

A3: for a being Element of (product F) holds
( a in product Z iff a in center (product F) )

proof

let a be Element of (product F); :: thesis: ( a in product Z iff a in center (product F) )

hereby :: thesis: ( a in center (product F) implies a in product Z )

assume a in product Z ; :: thesis: a in center (product F)
then for b being Element of (product F) holds a * b = b * a by A2;
hence a in center (product F) by GROUP_5:77; :: thesis: verum

end;

assume a in center (product F) ; :: thesis: a in product Z
then for b being Element of (product F) holds a * b = b * a by GROUP_5:77;
hence a in product Z by A2; :: thesis: verum

end;

for i being Element of I holds Z . i is Subgroup of F . i

proof

let i be Element of I; :: thesis: Z . i is Subgroup of F . i
Z . i = center (F . i) by A1;
hence Z . i is Subgroup of F . i ; :: thesis: verum

end;

then product Z is Subgroup of product F by GROUP_21:23;
hence center (product F) = product Z by A3, GROUP_2:60; :: thesis: verum