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