let D be non empty 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> ) & the_unity_wrt the multF of (D *+^ ) = {} ) by Def22, Th19, Th69;
hence ( the carrier of (D *+^+<0> ) = D * & the multF of (D *+^+<0> ) = D -concatenation & 1. (D *+^+<0> ) = {} ) by Def34; :: thesis: verum