let I be finite set ; :: thesis: for F being Group-like associative multMagma-Family of I holds product F = sum F
let F be Group-like associative multMagma-Family of I; :: thesis:
set GP = product F;
set S = sum F;
A1: the carrier of (sum F) = the carrier of ()
proof
reconsider g = 1_ () as Element of product () by Def2;
thus the carrier of (sum F) c= the carrier of () by GROUP_2:def 5; :: according to XBOOLE_0:def 10 :: thesis: the carrier of () c= the carrier of (sum F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in the carrier of (sum F) )
assume x in the carrier of () ; :: thesis: x in the carrier of (sum F)
then reconsider f = x as Element of product () by Def2;
A2: for p being Element of product () holds dom p = I by PARTFUN1:def 2;
then A3: dom f = I ;
reconsider f = f as ManySortedSet of I ;
ex g being Element of product () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
proof
deffunc H1( object ) -> set = f . \$1;
defpred S1[ object ] means ex G being non empty Group-like multMagma ex m being Element of G st
( G = F . \$1 & m = f . \$1 & m <> 1_ G );
consider J being set such that
A4: for j being object holds
( j in J iff ( j in I & S1[j] ) ) from J c= I by A4;
then reconsider J = J as Subset of I ;
consider ff being ManySortedSet of J such that
A5: for j being object st j in J holds
ff . j = H1(j) from PBOOLE:sch 4();
A6: dom ff = J by PARTFUN1:def 2;
A7: now :: thesis: for i being object st i in I holds
f . i = (g +* ff) . i
let i be object ; :: thesis: ( i in I implies f . b1 = (g +* ff) . b1 )
assume A8: i in I ; :: thesis: f . b1 = (g +* ff) . b1
per cases ( i in J or not i in J ) ;
suppose A9: i in J ; :: thesis: f . b1 = (g +* ff) . b1
hence f . i = ff . i by A5
.= (g +* ff) . i by ;
:: thesis: verum
end;
suppose A10: not i in J ; :: thesis: f . b1 = (g +* ff) . b1
consider G being non empty Group-like multMagma such that
A11: G = F . i by ;
f . i is Element of G by A8, A11, Lm1;
hence f . i = 1_ G by A4, A8, A10, A11
.= g . i by A8, A11, Th6
.= (g +* ff) . i by ;
:: thesis: verum
end;
end;
end;
take g ; :: thesis: ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )

take J ; :: thesis: ex f being ManySortedSet of J st
( g = 1_ () & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )

take ff ; :: thesis: ( g = 1_ () & x = g +* ff & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) )

thus g = 1_ () ; :: thesis: ( x = g +* ff & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) )

A12: dom g = I by A2;
dom (g +* ff) = (dom g) \/ (dom ff) by FUNCT_4:def 1
.= I by ;
hence x = g +* ff by ; :: thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )

let j be set ; :: thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) )

assume A13: j in J ; :: thesis: ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )

then consider G being non empty Group-like multMagma , m being Element of G such that
A14: G = F . j and
A15: m = f . j and
A16: m <> 1_ G by A4;
take G ; :: thesis: ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )
ff . j = f . j by ;
hence ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) by ; :: thesis: verum
end;
hence x in the carrier of (sum F) by Def9; :: thesis: verum
end;
product F is Subgroup of product F by GROUP_2:54;
hence product F = sum F by ; :: thesis: verum