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