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 ;
the multF of H = the multF of G || the carrier of H by ;
then A4: H is Subgroup of G by ;
now :: thesis: for o being Element of O holds H ^ o = (G ^ o) | the carrier of H
let o be Element of O; :: thesis: H ^ o = (G ^ o) | the carrier of H
reconsider 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 ;
A6: now :: thesis: for x being object st x in dom f holds
f . x = f9 . x
let x be object ; :: thesis: ( x in dom f implies f . x = f9 . x )
assume A7: x in dom f ; :: thesis: f . x = f9 . x
then A8: x in dom (id the carrier of H) by A2, A5;
x in {(1_ G)} by ;
then A9: x = 1_ G by TARSKI:def 1;
then x = 1_ H by ;
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
.= (G ^ o) . x by
.= 1_ G by ;
hence f . x = f9 . x by ; :: thesis: verum
end;
dom f9 = the carrier of ((1). G) by ;
hence H ^ o = (G ^ o) | the carrier of H by ; :: thesis: verum
end;
then reconsider H = H as strict StableSubgroup of G by ;
take H ; :: thesis: the carrier of H = {(1_ G)}
thus the carrier of H = {(1_ G)} by ; :: thesis: verum