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 associative holds

G is associative

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

G is associative

let G be non empty multMagma ; :: thesis: ( i in I & G = F . i & product F is associative implies G is associative )

assume that

A1: i in I and

A2: G = F . i and

A3: for x, y, z being Element of (product F) holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def 3 :: thesis: G is associative

let x, y, z be Element of G; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)

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);

A8: dom gy = I by PARTFUN1:def 2;

_{2}[ object , object ] means ( ( $1 = i implies $2 = z ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st

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

A13: for j being object st j in I holds

ex k being object st S_{2}[j,k]

A16: for j being object st j in I holds

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

set GP = product F;

defpred S_{3}[ 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 ) ) );

A17: for j being object st j in I holds

ex k being object st S_{3}[j,k]

A20: for j being object st j in I holds

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

A21: dom gx = I by PARTFUN1:def 2;

then reconsider gx = gx as Element of product (Carrier F) by A21, A22, CARD_3:9;

reconsider gz = gz as Element of product (Carrier F) by A26, A31, A27, CARD_3:9;

reconsider gy = gy as Element of product (Carrier F) by A8, A31, A9, CARD_3:9;

reconsider x1 = gx, y1 = gy, z1 = gz as Element of (product F) by Def2;

reconsider xy = x1 * y1, xyz3 = (x1 * y1) * z1, yz = y1 * z1, xyz5 = x1 * (y1 * z1) as Element of product (Carrier F) by Def2;

reconsider xyi = xy . i, yzi = yz . i as Element of G by A1, A2, Lm1;

A32: (x1 * y1) * z1 = x1 * (y1 * z1) by A3;

A33: gx . i = x by A1, A20;

then A34: x * yzi = xyz5 . i by A1, A2, Th1;

A35: gz . i = z by A1, A16;

then A36: xyi * z = xyz3 . i by A1, A2, Th1;

A37: gy . i = y by A1, A7;

then xy . i = x * y by A1, A2, A33, Th1;

hence (x * y) * z = x * (y * z) by A1, A2, A32, A37, A35, A36, A34, Th1; :: thesis: verum

for G being non empty multMagma st i in I & G = F . i & product F is associative holds

G is associative

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

G is associative

let G be non empty multMagma ; :: thesis: ( i in I & G = F . i & product F is associative implies G is associative )

assume that

A1: i in I and

A2: G = F . i and

A3: for x, y, z being Element of (product F) holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def 3 :: thesis: G is associative

let x, y, z be Element of G; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)

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

A8: dom gy = I by PARTFUN1:def 2;

A9: now :: thesis: for j being object st j in dom gy holds

gy . j in (Carrier F) . j

defpred Sgy . j in (Carrier F) . j

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

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

then A11: ex R being 1-sorted st

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

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

then A11: ex R being 1-sorted st

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

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

A13: for j being object st j in I holds

ex k being object st S

proof

consider gz 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 A14: j in I ; :: thesis: ex k being object st S_{2}[j,k]

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

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

end;

suppose A15:
j <> i
; :: thesis: ex k being object st S_{2}[j,k]

j in dom F
by A14, 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 = z ) by A15; :: 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 = z ) by A15; :: 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

A16: for j being object st j in I holds

S

set GP = product F;

defpred S

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

A17: 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_{3}[j,k] )

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

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

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

end;

suppose A19:
j <> i
; :: thesis: ex k being object st S_{3}[j,k]

j in dom F
by A18, 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_{3}[j, the Element of Fj]

thus ( j = i implies the Element of Fj = x ) by A19; :: 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 A19; :: 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

A20: for j being object st j in I holds

S

A21: dom gx = I by PARTFUN1:def 2;

A22: now :: thesis: for j being object st j in dom gx holds

gx . j in (Carrier F) . j

A26:
dom gz = I
by PARTFUN1:def 2;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 A23: j in dom gx ; :: thesis: gx . b_{1} in (Carrier F) . b_{1}

then A24: ex R being 1-sorted st

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

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

then A24: ex R being 1-sorted st

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

A27: now :: thesis: for j being object st j in dom gz holds

gz . j in (Carrier F) . j

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

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

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

then A29: ex R being 1-sorted st

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

end;assume A28: j in dom gz ; :: thesis: gz . b

then A29: ex R being 1-sorted st

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

then reconsider gx = gx as Element of product (Carrier F) by A21, A22, CARD_3:9;

reconsider gz = gz as Element of product (Carrier F) by A26, A31, A27, CARD_3:9;

reconsider gy = gy as Element of product (Carrier F) by A8, A31, A9, CARD_3:9;

reconsider x1 = gx, y1 = gy, z1 = gz as Element of (product F) by Def2;

reconsider xy = x1 * y1, xyz3 = (x1 * y1) * z1, yz = y1 * z1, xyz5 = x1 * (y1 * z1) as Element of product (Carrier F) by Def2;

reconsider xyi = xy . i, yzi = yz . i as Element of G by A1, A2, Lm1;

A32: (x1 * y1) * z1 = x1 * (y1 * z1) by A3;

A33: gx . i = x by A1, A20;

then A34: x * yzi = xyz5 . i by A1, A2, Th1;

A35: gz . i = z by A1, A16;

then A36: xyi * z = xyz3 . i by A1, A2, Th1;

A37: gy . i = y by A1, A7;

then xy . i = x * y by A1, A2, A33, Th1;

hence (x * y) * z = x * (y * z) by A1, A2, A32, A37, A35, A36, A34, Th1; :: thesis: verum