set G' = (1). G;
consider H being non empty HGrWOpStr of O such that
A1:
( H is strict & H is distributive & H is Group-like & H is associative & (1). G = multMagma(# the carrier of H,the multF of H #) )
by Lm3;
reconsider H = H as strict GroupWithOperators of O by A1;
A2:
( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H )
by A1, GROUP_2:def 5;
then A3:
H is Subgroup of G
by GROUP_2:def 5;
now let o be
Element of
O;
:: thesis: H ^ o = (G ^ o) | the carrier of Hreconsider f' =
H ^ o,
f =
(G ^ o) | the
carrier of
H as
Function ;
A4:
dom f' = the
carrier of
((1). G)
by A1, FUNCT_2:def 1;
A5:
dom f =
dom ((G ^ o) * (id the carrier of H))
by RELAT_1:94
.=
(dom (G ^ o)) /\ the
carrier of
H
by FUNCT_1:37
.=
the
carrier of
G /\ the
carrier of
H
by FUNCT_2:def 1
.=
the
carrier of
((1). G)
by A1, A2, XBOOLE_1:28
;
now let x be
set ;
:: thesis: ( x in dom f implies f . x = f' . x )assume A6:
x in dom f
;
:: thesis: f . x = f' . xthen
x in {(1_ G)}
by A5, GROUP_2:def 7;
then A7:
x = 1_ G
by TARSKI:def 1;
then
x = 1_ H
by A3, GROUP_2:53;
then A8:
f' . x = 1_ H
by GROUP_6:40;
A9:
x in dom (id the carrier of H)
by A1, A5, A6, RELAT_1:71;
f . x =
((G ^ o) * (id the carrier of H)) . x
by RELAT_1:94
.=
(G ^ o) . ((id the carrier of H) . x)
by A9, FUNCT_1:23
.=
(G ^ o) . x
by A1, A5, A6, FUNCT_1:35
.=
1_ G
by A7, GROUP_6:40
;
hence
f . x = f' . x
by A3, A8, GROUP_2:53;
:: thesis: verum end; hence
H ^ o = (G ^ o) | the
carrier of
H
by A4, A5, FUNCT_1:9;
:: thesis: verum end;
then reconsider H = H as strict StableSubgroup of G by A3, Def7;
take
H
; :: thesis: the carrier of H = {(1_ G)}
thus
the carrier of H = {(1_ G)}
by A1, GROUP_2:def 7; :: thesis: verum