theorem Th61: :: MONOID_0:61

for D being set holds
( the carrier of (D *+^+<0>) = D * & the multF of (D *+^+<0>) = D -concatenation & 1. (D *+^+<0>) = {} )