consider a being Element of G such that
A1:
for b being Element of G holds
( a * b = b & b * a = b )
by Th6;
A2:
a = a * a
by A1;
set f = the BinOp of {a};
set H = multMagma(# {a}, the BinOp of {a} #);
A3:
dom H2(G) = [:H1(G),H1(G):]
by FUNCT_2:def 1;
the BinOp of {a} =
(a,a) .--> a
by Th3
.=
[a,a] .--> a
;
then
H2( multMagma(# {a}, the BinOp of {a} #)) c= H2(G)
by A2, A3, FUNCT_4:7;
then reconsider H = multMagma(# {a}, the BinOp of {a} #) as non empty SubStr of G by Def23;
take
H
; ( H is unital & H is associative & H is commutative & H is cancelable & H is idempotent & H is invertible & H is uniquely-decomposable & H is strict )
thus
( H2(H) is having_a_unity & H2(H) is associative & H2(H) is commutative & H2(H) is cancelable & H2(H) is idempotent & H2(H) is invertible & H2(H) is uniquely-decomposable )
by Th3; MONOID_0:def 10,MONOID_0:def 11,MONOID_0:def 12,MONOID_0:def 13,MONOID_0:def 16,MONOID_0:def 19,MONOID_0:def 20 H is strict
thus
H is strict
; verum