let i, I be set ; for f being Function
for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let f be Function; for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let F be Group-like multMagma-Family of I; for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let G be non empty Group-like multMagma ; ( i in I & G = F . i & f = 1_ (product F) implies f . i = 1_ G )
assume that
A1:
i in I
and
A2:
G = F . i
and
A3:
f = 1_ (product F)
; f . i = 1_ G
set GP = product F;
f in the carrier of (product F)
by A3;
then A4:
f in product (Carrier F)
by Def2;
then reconsider e = f . i as Element of G by A1, A2, Lm1;
now for h being Element of G holds
( h * e = h & e * h = h )let h be
Element of
G;
( h * e = h & e * h = h )defpred S1[
object ,
object ]
means ( ( $1
= i implies $2
= h ) & ( $1
<> i implies ex
H being non
empty Group-like multMagma st
(
H = F . $1 & $2
= 1_ H ) ) );
A5:
for
j being
object st
j in I holds
ex
k being
object st
S1[
j,
k]
consider g being
ManySortedSet of
I such that A9:
for
j being
object st
j in I holds
S1[
j,
g . j]
from PBOOLE:sch 3(A5);
A10:
dom g = I
by PARTFUN1:def 2;
dom (Carrier F) = I
by PARTFUN1:def 2;
then A15:
g in product (Carrier F)
by A10, A11, CARD_3:9;
then reconsider g1 =
g as
Element of
(product F) by Def2;
A16:
g1 * (1_ (product F)) = g1
by GROUP_1:def 4;
A17:
g . i = h
by A1, A9;
A18:
g . i = h
by A1, A9;
ex
Fi being non
empty multMagma ex
m being
Function st
(
Fi = F . i &
m = the
multF of
(product F) . (
g,
f) &
m . i = the
multF of
Fi . (
(g . i),
(f . i)) )
by A1, A4, A15, Def2;
hence
h * e = h
by A2, A3, A16, A18;
e * h = hA19:
(1_ (product F)) * g1 = g1
by GROUP_1:def 4;
ex
Fi being non
empty multMagma ex
m being
Function st
(
Fi = F . i &
m = the
multF of
(product F) . (
f,
g) &
m . i = the
multF of
Fi . (
(f . i),
(g . i)) )
by A1, A4, A15, Def2;
hence
e * h = h
by A2, A3, A19, A17;
verum end;
hence
f . i = 1_ G
by GROUP_1:4; verum