let I, i be set ; :: thesis: for F being multMagma-Family of
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 ; :: 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 & G = F . i ) and
A2: for x, y being Element of (product F) holds x * y = y * x ; :: according to GROUP_1:def 16 :: thesis: G is commutative
set GP = product F;
let x, y be Element of G; :: according to GROUP_1:def 16 :: thesis: x * y = y * x
defpred S₁[ set , set ] 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 ) ) );
A3: for j being set st j in I holds
ex k being set st S₁[j,k]

proof

let j be set ; :: thesis: ( j in I implies ex k being set st S₁[j,k] )
assume A4: j in I ; :: thesis: ex k being set st S₁[j,k]

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: ex k being set st S₁[j,k]

hence ex k being set st S₁[j,k] ; :: thesis: verum

end;

suppose A5: j <> i ; :: thesis: ex k being set st S₁[j,k]

j in dom F by A4, PARTFUN1:def 4;
then F . j in rng F by FUNCT_1:def 5;
then reconsider Fj = F . j as non empty multMagma by Def1;
consider a being Element of Fj;
take a ; :: thesis: S₁[j,a]
thus ( j = i implies a = x ) by A5; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & a = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & a = a ) ) ; :: thesis: verum

end;

end;

end;

consider gx being ManySortedSet of such that
A6: for j being set st j in I holds
S₁[j,gx . j] from PBOOLE:sch 3(A3);
defpred S₂[ set , set ] 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 ) ) );
A7: for j being set st j in I holds
ex k being set st S₂[j,k]

proof

let j be set ; :: thesis: ( j in I implies ex k being set st S₂[j,k] )
assume A8: j in I ; :: thesis: ex k being set st S₂[j,k]

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: ex k being set st S₂[j,k]

hence ex k being set st S₂[j,k] ; :: thesis: verum

end;

suppose A9: j <> i ; :: thesis: ex k being set st S₂[j,k]

j in dom F by A8, PARTFUN1:def 4;
then F . j in rng F by FUNCT_1:def 5;
then reconsider Fj = F . j as non empty multMagma by Def1;
consider a being Element of Fj;
take a ; :: thesis: S₂[j,a]
thus ( j = i implies a = y ) by A9; :: thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & a = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & a = a ) ) ; :: thesis: verum

end;

end;

end;

consider gy being ManySortedSet of such that
A10: for j being set st j in I holds
S₂[j,gy . j] from PBOOLE:sch 3(A7);
A11: ( dom gx = I & dom gy = I ) by PARTFUN1:def 4;
A12: dom (Carrier F) = I by PARTFUN1:def 4;

now

let j be set ; :: thesis: ( j in dom gx implies gx . b₁ in (Carrier F) . b₁ )
assume A13: j in dom gx ; :: thesis: gx . b₁ in (Carrier F) . b₁
then consider R being 1-sorted such that
A14: ( R = F . j & (Carrier F) . j = the carrier of R ) by A11, PRALG_1:def 13;

per cases ( i = j or j <> i ) ;

suppose A15: i = j ; :: thesis: gx . b₁ in (Carrier F) . b₁

then gx . j = x by A6, A11, A13;
hence gx . j in (Carrier F) . j by A1, A14, A15; :: thesis: verum

end;

suppose j <> i ; :: thesis: gx . b₁ in (Carrier F) . b₁

then consider H being non empty multMagma , a being Element of H such that
A16: ( H = F . j & gx . j = a ) by A6, A11, A13;
thus gx . j in (Carrier F) . j by A14, A16; :: thesis: verum

end;

end;

end;

then reconsider gx = gx as Element of product (Carrier F) by A11, A12, CARD_3:18;

now

let j be set ; :: thesis: ( j in dom gy implies gy . b₁ in (Carrier F) . b₁ )
assume A17: j in dom gy ; :: thesis: gy . b₁ in (Carrier F) . b₁
then consider R being 1-sorted such that
A18: ( R = F . j & (Carrier F) . j = the carrier of R ) by A11, PRALG_1:def 13;

per cases ( i = j or j <> i ) ;

suppose A19: i = j ; :: thesis: gy . b₁ in (Carrier F) . b₁

then gy . j = y by A10, A11, A17;
hence gy . j in (Carrier F) . j by A1, A18, A19; :: thesis: verum

end;

suppose j <> i ; :: thesis: gy . b₁ in (Carrier F) . b₁

then consider H being non empty multMagma , a being Element of H such that
A20: ( H = F . j & gy . j = a ) by A10, A11, A17;
thus gy . j in (Carrier F) . j by A18, A20; :: thesis: verum

end;

end;

end;

then reconsider gy = gy as Element of product (Carrier F) by A11, A12, CARD_3:18;
reconsider x1 = gx, y1 = gy as Element of (product F) by Def2;
reconsider xy = x1 * y1 as Element of product (Carrier F) by Def2;
A21: x1 * y1 = y1 * x1 by A2;
A22: ( gx . i = x & gy . i = y ) by A1, A6, A10;
then xy . i = x * y by A1, Th4;
hence x * y = y * x by A1, A21, A22, Th4; :: thesis: verum