let i, I be set ; :: thesis: for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is commutative holds
G is commutative

let F be multMagma-Family of I; :: thesis: for G being non empty multMagma st i in I & G = F . i & product F is commutative holds
G is commutative

let G be non empty multMagma ; :: thesis: ( i in I & G = F . i & product F is commutative implies G is commutative )
assume that
A1: i in I and
A2: G = F . i and
A3: for x, y being Element of () holds x * y = y * x ; :: according to GROUP_1:def 12 :: thesis: G is commutative
let x, y be Element of G; :: according to GROUP_1:def 12 :: thesis: x * y = y * x
defpred S1[ object , object ] means ( ( \$1 = i implies \$2 = y ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . \$1 & \$2 = a ) ) );
A4: for j being object st j in I holds
ex k being object st S1[j,k]
proof
let j be object ; :: thesis: ( j in I implies ex k being object st S1[j,k] )
assume A5: j in I ; :: thesis: ex k being object st S1[j,k]
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: ex k being object st S1[j,k]
hence ex k being object st S1[j,k] ; :: thesis: verum
end;
suppose A6: j <> i ; :: thesis: ex k being object st S1[j,k]
j in dom F by ;
then F . j in rng F by FUNCT_1:def 3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; :: thesis: S1[j, the Element of Fj]
thus ( j = i implies the Element of Fj = y ) by A6; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )

thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; :: thesis: verum
end;
end;
end;
consider gy being ManySortedSet of I such that
A7: for j being object st j in I holds
S1[j,gy . j] from set GP = product F;
defpred S2[ object , object ] means ( ( \$1 = i implies \$2 = x ) & ( \$1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . \$1 & \$2 = a ) ) );
A8: for j being object st j in I holds
ex k being object st S2[j,k]
proof
let j be object ; :: thesis: ( j in I implies ex k being object st S2[j,k] )
assume A9: j in I ; :: thesis: ex k being object st S2[j,k]
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: ex k being object st S2[j,k]
hence ex k being object st S2[j,k] ; :: thesis: verum
end;
suppose A10: j <> i ; :: thesis: ex k being object st S2[j,k]
j in dom F by ;
then F . j in rng F by FUNCT_1:def 3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; :: thesis: S2[j, the Element of Fj]
thus ( j = i implies the Element of Fj = x ) by A10; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )

thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; :: thesis: verum
end;
end;
end;
consider gx being ManySortedSet of I such that
A11: for j being object st j in I holds
S2[j,gx . j] from A12: dom gy = I by PARTFUN1:def 2;
A13: now :: thesis: for j being object st j in dom gy holds
gy . j in () . j
let j be object ; :: thesis: ( j in dom gy implies gy . b1 in () . b1 )
assume A14: j in dom gy ; :: thesis: gy . b1 in () . b1
then A15: ex R being 1-sorted st
( R = F . j & () . j = the carrier of R ) by PRALG_1:def 15;
per cases ( i = j or j <> i ) ;
suppose A16: i = j ; :: thesis: gy . b1 in () . b1
then gy . j = y by ;
hence gy . j in () . j by A2, A15, A16; :: thesis: verum
end;
suppose j <> i ; :: thesis: gy . b1 in () . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gy . j = a ) by ;
hence gy . j in () . j by A15; :: thesis: verum
end;
end;
end;
A17: dom () = I by PARTFUN1:def 2;
then reconsider gy = gy as Element of product () by ;
A18: gy . i = y by A1, A7;
A19: dom gx = I by PARTFUN1:def 2;
now :: thesis: for j being object st j in dom gx holds
gx . j in () . j
let j be object ; :: thesis: ( j in dom gx implies gx . b1 in () . b1 )
assume A20: j in dom gx ; :: thesis: gx . b1 in () . b1
then A21: ex R being 1-sorted st
( R = F . j & () . j = the carrier of R ) by PRALG_1:def 15;
per cases ( i = j or j <> i ) ;
suppose A22: i = j ; :: thesis: gx . b1 in () . b1
then gx . j = x by ;
hence gx . j in () . j by A2, A21, A22; :: thesis: verum
end;
suppose j <> i ; :: thesis: gx . b1 in () . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gx . j = a ) by ;
hence gx . j in () . j by A21; :: thesis: verum
end;
end;
end;
then reconsider gx = gx as Element of product () by ;
reconsider x1 = gx, y1 = gy as Element of () by Def2;
A23: x1 * y1 = y1 * x1 by A3;
reconsider xy = x1 * y1 as Element of product () by Def2;
A24: gx . i = x by ;
then xy . i = x * y by A1, A2, A18, Th1;
hence x * y = y * x by A1, A2, A23, A24, A18, Th1; :: thesis: verum