consider S being empty multMagma ;
reconsider A = the carrier of S as set ;
reconsider X = [:A,A:] as set ;
the multF of S = the multF of M | {}
.= the multF of M | X by ZFMISC_1:113
.= the multF of M || the carrier of S by REALSET1:def 3 ;
hence ex b₁ being multMagma st
( the carrier of b₁ c= the carrier of M & the multF of b₁ = the multF of M || the carrier of b₁ ) by XBOOLE_1:2; :: thesis: verum