let I be set ; for s being ManySortedSet of I
for F being Group-like multMagma-Family of I st ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) holds
s = 1_ (product F)
let s be ManySortedSet of I; for F being Group-like multMagma-Family of I st ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) holds
s = 1_ (product F)
let F be Group-like multMagma-Family of I; ( ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) implies s = 1_ (product F) )
assume A1:
for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G )
; s = 1_ (product F)
set GP = product F;
A2:
dom (Carrier F) = I
by PARTFUN1:def 2;
A3:
dom s = I
by PARTFUN1:def 2;
then A6:
s in product (Carrier F)
by A3, A2, CARD_3:9;
then reconsider e = s as Element of (product F) by Def2;
now for h being Element of (product F) holds
( h * e = h & e * h = h )let h be
Element of
(product F);
( h * e = h & e * h = h )reconsider h1 =
h,
he =
h * e,
eh =
e * h as
Element of
product (Carrier F) by Def2;
A7:
dom h1 = I
by A2, CARD_3:9;
A8:
now for i being object st i in I holds
he . i = h1 . ilet i be
object ;
( i in I implies he . i = h1 . i )assume A9:
i in I
;
he . i = h1 . ithen consider G being non
empty Group-like multMagma such that A10:
G = F . i
and A11:
s . i = 1_ G
by A1;
reconsider b =
h1 . i,
c =
s . i as
Element of
G by A9, A10, A11, Lm1;
A12:
ex
Fi being non
empty multMagma ex
m being
Function st
(
Fi = F . i &
m = the
multF of
(product F) . (
h,
s) &
m . i = the
multF of
Fi . (
(h1 . i),
(s . i)) )
by A6, A9, Def2;
b * c = b
by A11, GROUP_1:def 4;
hence
he . i = h1 . i
by A12, A10;
verum end;
dom he = I
by A2, CARD_3:9;
hence
h * e = h
by A7, A8;
e * h = hA13:
now for i being object st i in I holds
eh . i = h1 . ilet i be
object ;
( i in I implies eh . i = h1 . i )assume A14:
i in I
;
eh . i = h1 . ithen consider G being non
empty Group-like multMagma such that A15:
G = F . i
and A16:
s . i = 1_ G
by A1;
reconsider b =
h1 . i,
c =
s . i as
Element of
G by A14, A15, A16, Lm1;
A17:
ex
Fi being non
empty multMagma ex
m being
Function st
(
Fi = F . i &
m = the
multF of
(product F) . (
s,
h) &
m . i = the
multF of
Fi . (
(s . i),
(h1 . i)) )
by A6, A14, Def2;
c * b = b
by A16, GROUP_1:def 4;
hence
eh . i = h1 . i
by A17, A15;
verum end;
dom eh = I
by A2, CARD_3:9;
hence
e * h = h
by A7, A13;
verum end;
hence
s = 1_ (product F)
by GROUP_1:4; verum