set a = H₃(G);
reconsider e = H₃(G) as Element of {H₃(G)} by TARSKI:def 1;
consider f being BinOp of {H₃(G)};
set H = multLoopStr(# {H₃(G)},f,e #);
A1: 1. multLoopStr(# {H₃(G)},f,e #) = 1. G ;
X: [H₃(G),H₃(G)] .--> H₃(G) = {[H₃(G),H₃(G)]} --> H₃(G) ;
( f = H₃(G),H₃(G) .--> H₃(G) & H₃(G) = H₃(G) * H₃(G) & H₃(G) * H₃(G) = H₂(G) . H₃(G),H₃(G) & dom H₂(G) = [:H₁(G),H₁(G):] ) by Th3, Th18, FUNCT_2:def 1;
then H₂( multLoopStr(# {H₃(G)},f,e #)) c= H₂(G) by FUNCT_4:8, X;
then reconsider H = multLoopStr(# {H₃(G)},f,e #) as non empty MonoidalSubStr of G by A1, Def25;
take H ; :: thesis: ( H is well-unital & H is associative & H is commutative & H is cancelable & H is idempotent & H is invertible & H is uniquely-decomposable & H is strict )

now

let b be Element of H; :: thesis: ( H₂(H) . H₃(H),b = b & H₂(H) . b,H₃(H) = b )
b = H₃(G) by TARSKI:def 1;
hence ( H₂(H) . H₃(H),b = b & H₂(H) . b,H₃(H) = b ) by TARSKI:def 1; :: thesis: verum

end;

hence H₃(H) is_a_unity_wrt H₂(H) by BINOP_1:11; :: according to MONOID_0:def 21 :: thesis: ( H is associative & H is commutative & H is cancelable & H is idempotent & H is invertible & H is uniquely-decomposable & H is strict )
thus ( H₂(H) is associative & H₂(H) is commutative & H₂(H) is cancelable & H₂(H) is idempotent & H₂(H) is invertible & H₂(H) is uniquely-decomposable ) by Th3; :: according to 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