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 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 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: 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 PBOOLE:sch 3(A4);
 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
let j be object ; :: thesis: ( j in dom gy implies gy . b1 in (Carrier F) . b1 )
assume A10: j in dom gy ; :: thesis: gy . b1 in (Carrier F) . b1
then A11: 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 A12: i = j ; :: thesis: gy . b1 in (Carrier F) . b1
then gy . j = y by A7, A10;
hence gy . j in (Carrier F) . j by A2, A11, A12; :: thesis: verum
end;
suppose j <> i ; :: thesis: gy . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gy . j = a ) by A7, A10;
hence gy . j in (Carrier F) . j by A11; :: thesis: verum
end;
end;
end;
defpred S2[ 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 S2[j,k]
proof
let j be object ; :: thesis: ( j in I implies ex k being object st S2[j,k] )
assume A14: 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 A15: j <> i ; :: thesis: ex k being object st S2[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: S2[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;
end;
end;
consider gz being ManySortedSet of I such that
A16: for j being object st j in I holds
S2[j,gz . j] from PBOOLE:sch 3(A13);
 set GP = product F;
defpred S3[ 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 S3[j,k]
proof
let j be object ; :: thesis: ( j in I implies ex k being object st S3[j,k] )
assume A18: j in I ; :: thesis: ex k being object st S3[j,k]
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: ex k being object st S3[j,k]
hence ex k being object st S3[j,k] ; :: thesis: verum
end;
suppose A19: j <> i ; :: thesis: ex k being object st S3[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: S3[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;
end;
end;
consider gx being ManySortedSet of I such that
A20: for j being object st j in I holds
S3[j,gx . j] from PBOOLE:sch 3(A17);
 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
let j be object ; :: thesis: ( j in dom gx implies gx . b1 in (Carrier F) . b1 )
assume A23: j in dom gx ; :: thesis: gx . b1 in (Carrier F) . b1
then A24: 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 A25: i = j ; :: thesis: gx . b1 in (Carrier F) . b1
then gx . j = x by A20, A23;
hence gx . j in (Carrier F) . j by A2, A24, A25; :: thesis: verum
end;
suppose j <> i ; :: thesis: gx . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gx . j = a ) by A20, A23;
hence gx . j in (Carrier F) . j by A24; :: thesis: verum
end;
end;
end;
A26: dom gz = I by PARTFUN1:def 2;
A27: now :: thesis: for j being object st j in dom gz holds
gz . j in (Carrier F) . j
let j be object ; :: thesis: ( j in dom gz implies gz . b1 in (Carrier F) . b1 )
assume A28: j in dom gz ; :: thesis: gz . b1 in (Carrier F) . b1
then A29: 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 A30: i = j ; :: thesis: gz . b1 in (Carrier F) . b1
then gz . j = z by A16, A28;
hence gz . j in (Carrier F) . j by A2, A29, A30; :: thesis: verum
end;
suppose j <> i ; :: thesis: gz . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gz . j = a ) by A16, A28;
hence gz . j in (Carrier F) . j by A29; :: thesis: verum
end;
end;
end;
A31: dom (Carrier F) = 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