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_{1}[ 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_{1}[j,k]

A7: for j being object st j in I holds

S_{1}[j,gy . j]
from PBOOLE:sch 3(A4);

set GP = product F;

defpred S_{2}[ 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_{2}[j,k]

A11: for j being object st j in I holds

S_{2}[j,gx . j]
from PBOOLE:sch 3(A8);

A12: dom gy = 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;

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

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

( H = F . $1 & $2 = a ) ) );

A4: for j being object st j in I holds

ex k being object st S

proof

consider gy being ManySortedSet of I such that
let j be object ; :: thesis: ( j in I implies ex k being object st S_{1}[j,k] )

assume A5: j in I ; :: thesis: ex k being object st S_{1}[j,k]

end;assume A5: j in I ; :: thesis: ex k being object st S

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

end;

suppose A6:
j <> i
; :: thesis: ex k being object st S_{1}[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_{1}[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;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

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

A7: for j being object st j in I holds

S

set GP = product F;

defpred S

( H = F . $1 & $2 = a ) ) );

A8: for j being object st j in I holds

ex k being object st S

proof

consider gx being ManySortedSet of I such that
let j be object ; :: thesis: ( j in I implies ex k being object st S_{2}[j,k] )

assume A9: j in I ; :: thesis: ex k being object st S_{2}[j,k]

end;assume A9: j in I ; :: thesis: ex k being object st S

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

end;

suppose A10:
j <> i
; :: thesis: ex k being object st S_{2}[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_{2}[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;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

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

A11: for j being object st j in I holds

S

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

A17:
dom (Carrier F) = I
by PARTFUN1:def 2;gy . j in (Carrier F) . j

let j be object ; :: thesis: ( j in dom gy implies gy . b_{1} in (Carrier F) . b_{1} )

assume A14: j in dom gy ; :: thesis: gy . b_{1} in (Carrier F) . b_{1}

then A15: ex R being 1-sorted st

( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 13;

end;assume A14: j in dom gy ; :: thesis: gy . b

then A15: ex R being 1-sorted st

( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 13;

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

then reconsider gx = gx as Element of product (Carrier F) by A19, A17, CARD_3:9;gx . j in (Carrier F) . j

let j be object ; :: thesis: ( j in dom gx implies gx . b_{1} in (Carrier F) . b_{1} )

assume A20: j in dom gx ; :: thesis: gx . b_{1} in (Carrier F) . b_{1}

then A21: ex R being 1-sorted st

( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 13;

end;assume A20: j in dom gx ; :: thesis: gx . b

then A21: ex R being 1-sorted st

( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def 13;

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