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:

let b be Element of H; :: thesis:
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:

end;