set a = H3(G);
reconsider e = H3(G) as Element of {H3(G)} by TARSKI:def 1;
set f = the BinOp of {H3(G)};
set H = multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #);
A1:
( H3(G) = H3(G) * H3(G) & dom H2(G) = [:H1(G),H1(G):] )
by Th16, FUNCT_2:def 1;
( [H3(G),H3(G)] .--> H3(G) = {[H3(G),H3(G)]} --> H3(G) & the BinOp of {H3(G)} = (H3(G),H3(G)) .--> H3(G) )
by Th3;
then
( 1. multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #) = 1. G & H2( multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #)) c= H2(G) )
by A1, FUNCT_4:7;
then reconsider H = multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #) as non empty MonoidalSubStr of G by Def25;
take
H
; ( 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 for b being Element of H holds
( H2(H) . (H3(H),b) = b & H2(H) . (b,H3(H)) = b )end;
hence
H3(H) is_a_unity_wrt H2(H)
by BINOP_1:3; MONOID_0:def 21 ( 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 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 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