let I be finite set ; 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; product F = sum F
set GP = product F;
set S = sum F;
A1:
the carrier of (sum F) = the carrier of (product F)
proof
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;
XBOOLE_0:def 10 the carrier of (product F) c= the carrier of (sum F)
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (product F) or x in the carrier of (sum F) )
assume
x in the
carrier of
(product F)
;
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
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 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 = H1(
j)
from PBOOLE:sch 4();
A6:
dom ff = J
by PARTFUN1:def 2;
A7:
now for i being object st i in I holds
f . i = (g +* ff) . ilet i be
object ;
( i in I implies f . b1 = (g +* ff) . b1 )assume A8:
i in I
;
f . b1 = (g +* ff) . b1per cases
( i in J or not i in J )
;
suppose A10:
not
i in J
;
f . b1 = (g +* ff) . b1consider 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
;
verum end; end;
take
g
;
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
;
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
;
( 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)
;
( 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;
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 ;
( 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
;
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
;
( 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;
verum
end;
hence
x in the
carrier of
(sum F)
by Def9;
verum
end;
product F is Subgroup of product F
by GROUP_2:54;
hence
product F = sum F
by A1, GROUP_2:59; verum