let I be finite set ; :: thesis: for F being Group-like associative HGrStr-Family of I holds product F = sum F
let F be Group-like associative HGrStr-Family of I; :: thesis: product F = sum F
set GP = product F;
set S = sum F;
A1: the carrier of (sum F) = the carrier of (product F)

proof

thus the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def 5; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (product F) c= the carrier of (sum F)
reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (product F) or x in the carrier of (sum F) )
assume x in the carrier of (product F) ; :: thesis: x in the carrier of (sum F)
then reconsider f = x as Element of product (Carrier F) by Def2;

A2: now

let p be Element of product (Carrier F); :: thesis: dom p = I
thus dom p = dom (Carrier F) by CARD_3:18
.= I by PBOOLE:def 3 ; :: thesis: verum

end;

then A3: dom f = I ;
then reconsider f = f as ManySortedSet of I by PBOOLE:def 3;
ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & 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

defpred S₁[ set ] 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 set holds
( j in J iff ( j in I & S₁[j] ) ) from XBOOLE_0:sch 1();
J c= I

proof

let j be set ; :: according to TARSKI:def 3 :: thesis: ( not j in J or j in I )
assume j in J ; :: thesis: j in I
hence j in I by A4; :: thesis: verum

end;

then reconsider J = J as Subset of I ;
take g ; :: thesis: ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & 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_ (product F) & 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 ) ) )
deffunc H₁( set ) -> set = f . $1;
consider ff being ManySortedSet of J such that
A5: for j being set st j in J holds
ff . j = H₁(j) from PBOOLE:sch 4();
take ff ; :: thesis: ( g = 1_ (product F) & 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_ (product F) ; :: 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 ) ) )
A6: dom ff = J by PBOOLE:def 3;
A7: dom g = I by A2;
A8: dom (g +* ff) = (dom g) \/ (dom ff) by FUNCT_4:def 1
.= I by A6, A7, XBOOLE_1:12 ;

now

let i be set ; :: thesis: ( i in I implies f . b₁ = (g +* ff) . b₁ )
assume A9: i in I ; :: thesis: f . b₁ = (g +* ff) . b₁

per cases ( i in J or not i in J ) ;

suppose A10: i in J ; :: thesis: f . b₁ = (g +* ff) . b₁

hence f . i = ff . i by A5
.= (g +* ff) . i by A6, A10, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A11: not i in J ; :: thesis: f . b₁ = (g +* ff) . b₁

consider G being non empty Group-like multMagma such that
A12: G = F . i by A9, Def3;
f . i is Element of G by A9, A12, Lm1;
hence f . i = 1_ G by A4, A9, A11, A12
.= g . i by A9, A12, Th9
.= (g +* ff) . i by A6, A11, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

hence x = g +* ff by A3, A8, FUNCT_1:9; :: 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 & m = f . j & 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 A5, A13;
hence ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) by A14; :: 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:63;
hence product F = sum F by A1, GROUP_2:68; :: thesis: verum