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 (product F) 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 S₁[ 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 S₁[j,k]

proof

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

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

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

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

end;

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

j in dom F by A5, PARTFUN1:def 2;
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: S₁[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
S₁[j,gy . j] from PBOOLE:sch 3(A4);
set GP = product F;
defpred S₂[ 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 S₂[j,k]

proof

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

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

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

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

end;

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

j in dom F by A9, PARTFUN1:def 2;
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: S₂[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
S₂[j,gx . j] from PBOOLE:sch 3(A8);
A12: dom gy = I by PARTFUN1:def 2;

A13: now :: thesis: for j being object st j in dom gy holds
gy . j in (Carrier F) . j

let j be object ; :: thesis: ( j in dom gy implies gy . b₁ in (Carrier F) . b₁ )
assume A14: j in dom gy ; :: thesis: gy . b₁ in (Carrier F) . b₁
then A15: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 15;

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

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

then gy . j = y by A7, A14;
hence gy . j in (Carrier F) . j by A2, A15, A16; :: thesis: verum

end;

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

then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gy . j = a ) by A7, A14;
hence gy . j in (Carrier F) . j by A15; :: thesis: verum

end;

end;

end;

A17: dom (Carrier F) = I by PARTFUN1:def 2;
then reconsider gy = gy as Element of product (Carrier F) by A12, A13, CARD_3:9;
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 (Carrier F) . j

let j be object ; :: thesis: ( j in dom gx implies gx . b₁ in (Carrier F) . b₁ )
assume A20: j in dom gx ; :: thesis: gx . b₁ in (Carrier F) . b₁
then A21: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 15;

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

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

then gx . j = x by A11, A20;
hence gx . j in (Carrier F) . j by A2, A21, A22; :: thesis: verum

end;

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

then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gx . j = a ) by A11, A20;
hence gx . j in (Carrier F) . j by A21; :: thesis: verum

end;

end;

end;

then reconsider gx = gx as Element of product (Carrier F) by A19, A17, CARD_3:9;
reconsider x1 = gx, y1 = gy as Element of (product F) by Def2;
A23: x1 * y1 = y1 * x1 by A3;
reconsider xy = x1 * y1 as Element of product (Carrier F) by Def2;
A24: gx . i = x by A1, A11;
then xy . i = x * y by A1, A2, A18, Th1;
hence x * y = y * x by A1, A2, A23, A24, A18, Th1; :: thesis: verum