set S = the empty multMagma ;
reconsider A = the carrier of the empty multMagma as set ;
reconsider X = [:A,A:] as set ;
the multF of the empty multMagma = the multF of M | X
.= the multF of M || the carrier of the empty multMagma by REALSET1:def 2 ;
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