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