set N = multMagma(# the carrier of M, the multF of M #);
the multF of multMagma(# the carrier of M, the multF of M #) = the multF of multMagma(# the carrier of M, the multF of M #) | [: the carrier of multMagma(# the carrier of M, the multF of M #), the carrier of multMagma(# the carrier of M, the multF of M #):]
.= the multF of M || the carrier of multMagma(# the carrier of M, the multF of M #) by REALSET1:def 2 ;
then reconsider N = multMagma(# the carrier of M, the multF of M #) as multSubmagma of M by Def9;
take N ; :: thesis: not N is empty
thus not N is empty ; :: thesis: verum