reconsider G = F₁() as non empty multMagma ;
reconsider D = F₂() 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. F₁() as Element of H by A2, A4;
set N = multLoopStr(# the carrier of H,the multF of H,e #);
multLoopStr(# the carrier of H,the multF of H,e #) is MonoidalSubStr of F₁()

proof

thus H₂( multLoopStr(# the carrier of H,the multF of H,e #)) c= H₂(F₁()) by Def23; :: according to MONOID_0:def 25 :: thesis: 1. multLoopStr(# the carrier of H,the multF of H,e #) = 1. F₁()
thus 1. multLoopStr(# the carrier of H,the multF of H,e #) = 1. F₁() ; :: thesis: verum

end;

then reconsider N = multLoopStr(# the carrier of H,the multF of H,e #) as non empty strict MonoidalSubStr of F₁() ;
take N ; :: thesis: the carrier of N = F₂()
thus the carrier of N = F₂() by A4; :: thesis: verum