let D be set ; :: thesis: ( the carrier of (D *+^+<0>) = D * & the multF of (D *+^+<0>) = D -concatenation & 1. (D *+^+<0>) = {} )
set M = D *+^+<0> ;
( multMagma(# the carrier of (D *+^+<0>), the multF of (D *+^+<0>) #) = D *+^ & the_unity_wrt H₂(D *+^+<0> ) = H₃(D *+^+<0> ) ) by Def22, Th17;
hence ( the carrier of (D *+^+<0>) = D * & the multF of (D *+^+<0>) = D -concatenation & 1. (D *+^+<0>) = {} ) by Def34, Th60; :: thesis: verum