consider a being Element of G such that
A1:
for b being Element of G holds
( a * b = b & b * a = b )
by Th6;
consider f being BinOp of {a};
set H = multMagma(# {a},f #);
X: f =
a,a .--> a
by Th3
.=
[a,a] .--> a
;
Y:
( a = a * a & a * a = H2(G) . a,a )
by A1;
( H2(G) . a,a = H2(G) . [a,a] & dom H2(G) = [:H1(G),H1(G):] )
by FUNCT_2:def 1;
then
H2( multMagma(# {a},f #)) c= H2(G)
by FUNCT_4:8, X, Y;
then reconsider H = multMagma(# {a},f #) as non empty SubStr of G by Def23;
take
H
; :: thesis: ( 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; :: according to 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 :: thesis: H is strict
thus
H is strict
; :: thesis: verum