set a = H₃(G);
reconsider e = H₃(G) as Element of {H₃(G)} by TARSKI:def 1;
set f = the BinOp of {H₃(G)};
set H = multLoopStr(# {H₃(G)}, the BinOp of {H₃(G)},e #);
A1: ( H₃(G) = H₃(G) * H₃(G) & dom H₂(G) = [:H₁(G),H₁(G):] ) by Th16, FUNCT_2:def 1;
( [H₃(G),H₃(G)] .--> H₃(G) = {[H₃(G),H₃(G)]} --> H₃(G) & the BinOp of {H₃(G)} = (H₃(G),H₃(G)) .--> H₃(G) ) by Th3;
then ( 1. multLoopStr(# {H₃(G)}, the BinOp of {H₃(G)},e #) = 1. G & H₂( multLoopStr(# {H₃(G)}, the BinOp of {H₃(G)},e #)) c= H₂(G) ) by A1, FUNCT_4:7;
then reconsider H = multLoopStr(# {H₃(G)}, the BinOp of {H₃(G)},e #) as non empty MonoidalSubStr of G by 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 :: thesis: for b being Element of H holds
( H₂(H) . (H₃(H),b) = b & H₂(H) . (b,H₃(H)) = b )

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:3; :: 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