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 associative holds
G is associative
let F be multMagma-Family of ; :: 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 & G = F . i ) and
A2: for x, y, z being Element of (product F) holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def 4 :: thesis: G is associative
set GP = product F;
let x, y, z be Element of G; :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
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);
defpred S₃[ set , set ] 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 ) ) );
A11: 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 A12: 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 A13: j <> i ; :: thesis: ex k being set st S₃[j,k]

j in dom F by A12, 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 = z ) by A13; :: 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 gz being ManySortedSet of such that
A14: for j being set st j in I holds
S₃[j,gz . j] from PBOOLE:sch 3(A11);
A15: ( dom gx = I & dom gy = I & dom gz = I ) by PARTFUN1:def 4;
A16: 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 A17: j in dom gx ; :: thesis: gx . 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 A15, PRALG_1:def 13;

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

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

then gx . j = x by A6, A15, A17;
hence gx . j in (Carrier F) . j by A1, A18, A19; :: 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
A20: ( H = F . j & gx . j = a ) by A6, A15, A17;
thus gx . j in (Carrier F) . j by A18, A20; :: thesis: verum

end;

end;

end;

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

now

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

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

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

then gy . j = y by A10, A15, A21;
hence gy . j in (Carrier F) . j by A1, A22, A23; :: 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
A24: ( H = F . j & gy . j = a ) by A10, A15, A21;
thus gy . j in (Carrier F) . j by A22, A24; :: thesis: verum

end;

end;

end;

then reconsider gy = gy as Element of product (Carrier F) by A15, A16, CARD_3:18;

now

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

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

suppose A27: i = j ; :: thesis: gz . b₁ in (Carrier F) . b₁

then gz . j = z by A14, A15, A25;
hence gz . j in (Carrier F) . j by A1, A26, A27; :: thesis: verum

end;

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

then consider H being non empty multMagma , a being Element of H such that
A28: ( H = F . j & gz . j = a ) by A14, A15, A25;
thus gz . j in (Carrier F) . j by A26, A28; :: thesis: verum

end;

end;

end;

then reconsider gz = gz as Element of product (Carrier F) by A15, A16, CARD_3:18;
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, Lm1;
A29: (x1 * y1) * z1 = x1 * (y1 * z1) by A2;
A30: ( gx . i = x & gy . i = y & gz . i = z ) by A1, A6, A10, A14;
then ( xy . i = x * y & xyi * z = xyz3 . i & x * yzi = xyz5 . i ) by A1, Th4;
hence (x * y) * z = x * (y * z) by A1, A29, A30, Th4; :: thesis: verum