reconsider G = F1() as non empty multMagma ;
reconsider D = F2() as non empty Subset of G ;
A3:
for x, y being Element of D holds x * y in D
by A1;
consider H being non empty strict SubStr of G such that
A4:
the carrier of H = D
from MONOID_0:sch 1(A3);
reconsider e = 1. F1() as Element of H by A2, A4;
set N = multLoopStr(# the carrier of H,the multF of H,e #);
( H2( multLoopStr(# the carrier of H,the multF of H,e #)) c= H2(F1()) & ( for M being multLoopStr st F1() = M holds
1. multLoopStr(# the carrier of H,the multF of H,e #) = 1. M ) )
by Def23;
then reconsider N = multLoopStr(# the carrier of H,the multF of H,e #) as non empty strict MonoidalSubStr of F1() by Def25;
take
N
; :: thesis: the carrier of N = F2()
thus
the carrier of N = F2()
by A4; :: thesis: verum