H₁(D *+^ ) = D * by Def34;
hence the multF of (D *+^) is BinOp of (D *) ; :: thesis: verum