set G9 = (1). G;
consider H being non empty HGrWOpStr over O such that
A1:
( H is strict & H is distributive & H is Group-like & H is associative )
and
A2:
(1). G = multMagma(# the carrier of H, the multF of H #)
by Lm2;
reconsider H = H as strict GroupWithOperators of O by A1;
A3:
the carrier of H c= the carrier of G
by A2, GROUP_2:def 5;
the multF of H = the multF of G || the carrier of H
by A2, GROUP_2:def 5;
then A4:
H is Subgroup of G
by A3, GROUP_2:def 5;
now for o being Element of O holds H ^ o = (G ^ o) | the carrier of Hlet o be
Element of
O;
H ^ o = (G ^ o) | the carrier of Hreconsider f9 =
H ^ o,
f =
(G ^ o) | the
carrier of
H as
Function ;
A5:
dom f =
dom ((G ^ o) * (id the carrier of H))
by RELAT_1:65
.=
(dom (G ^ o)) /\ the
carrier of
H
by FUNCT_1:19
.=
the
carrier of
G /\ the
carrier of
H
by FUNCT_2:def 1
.=
the
carrier of
((1). G)
by A2, A3, XBOOLE_1:28
;
A6:
now for x being object st x in dom f holds
f . x = f9 . xlet x be
object ;
( x in dom f implies f . x = f9 . x )assume A7:
x in dom f
;
f . x = f9 . xthen A8:
x in dom (id the carrier of H)
by A2, A5;
x in {(1_ G)}
by A5, A7, GROUP_2:def 7;
then A9:
x = 1_ G
by TARSKI:def 1;
then
x = 1_ H
by A4, GROUP_2:44;
then A10:
f9 . x = 1_ H
by GROUP_6:31;
f . x =
((G ^ o) * (id the carrier of H)) . x
by RELAT_1:65
.=
(G ^ o) . ((id the carrier of H) . x)
by A8, FUNCT_1:13
.=
(G ^ o) . x
by A2, A5, A7, FUNCT_1:18
.=
1_ G
by A9, GROUP_6:31
;
hence
f . x = f9 . x
by A4, A10, GROUP_2:44;
verum end;
dom f9 = the
carrier of
((1). G)
by A2, FUNCT_2:def 1;
hence
H ^ o = (G ^ o) | the
carrier of
H
by A5, A6, FUNCT_1:2;
verum end;
then reconsider H = H as strict StableSubgroup of G by A4, Def7;
take
H
; the carrier of H = {(1_ G)}
thus
the carrier of H = {(1_ G)}
by A2, GROUP_2:def 7; verum