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: product F = sum F

set GP = product F;

set S = sum F;

A1: the carrier of (sum F) = the carrier of (product F)

hence product F = sum F by A1, GROUP_2:59; :: thesis: verum

let F be Group-like associative multMagma-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

product F is Subgroup of product F
by GROUP_2:54;
reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2;

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)

let x be object ; :: 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: for p being Element of product (Carrier F) 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 (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 ) ) )

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

let x be object ; :: 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: for p being Element of product (Carrier F) 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 (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

hence
x in the carrier of (sum F)
by Def9; :: thesis: verum
deffunc H_{1}( object ) -> set = f . $1;

defpred S_{1}[ 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 & S_{1}[j] ) )
from XBOOLE_0:sch 1();

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 = H_{1}(j)
from PBOOLE:sch 4();

A6: dom ff = J by PARTFUN1:def 2;

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

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

A12: dom g = I by A2;

dom (g +* ff) = (dom g) \/ (dom ff) by FUNCT_4:def 1

.= I by A6, A12, XBOOLE_1:12 ;

hence x = g +* ff by A3, A7, FUNCT_1:2; :: 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 A5, A13;

hence ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) by A14, A15, A16; :: thesis: verum

end;defpred S

( 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 & S

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 = H

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

take
g
; :: thesis: ex J being finite Subset of I ex f being ManySortedSet of J st f . i = (g +* ff) . i

let i be object ; :: thesis: ( i in I implies f . b_{1} = (g +* ff) . b_{1} )

assume A8: i in I ; :: thesis: f . b_{1} = (g +* ff) . b_{1}

end;assume A8: i in I ; :: thesis: f . b

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

end;

suppose A10:
not i in J
; :: thesis: f . b_{1} = (g +* ff) . b_{1}

consider G being non empty Group-like multMagma such that

A11: G = F . i by A8, Def3;

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 A6, A10, FUNCT_4:11 ;

:: thesis: verum

end;A11: G = F . i by A8, Def3;

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 A6, A10, FUNCT_4:11 ;

:: thesis: verum

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

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

A12: dom g = I by A2;

dom (g +* ff) = (dom g) \/ (dom ff) by FUNCT_4:def 1

.= I by A6, A12, XBOOLE_1:12 ;

hence x = g +* ff by A3, A7, FUNCT_1:2; :: 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 A5, A13;

hence ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) by A14, A15, A16; :: thesis: verum

hence product F = sum F by A1, GROUP_2:59; :: thesis: verum