let D be non empty set ; :: thesis: the_unity_wrt the multF of (D *+^ ) = {}
set N = D *+^ ;
set f = H₂(D *+^ );
A1: ( H₁(D *+^ ) = D * & ( for p, q being Element of (D *+^ ) holds p [*] q = p ^ q ) ) by Def34;
{} = <*> D ;
then reconsider a = {} as Element of (D *+^ ) by A1, FINSEQ_1:def 11;

now

let b be Element of (D *+^ ); :: thesis: ( H₂(D *+^ ) . a,b = b & H₂(D *+^ ) . b,a = b )
thus H₂(D *+^ ) . a,b = a [*] b
.= {} ^ b by Def34
.= b by FINSEQ_1:47 ; :: thesis: H₂(D *+^ ) . b,a = b
thus H₂(D *+^ ) . b,a = b [*] a
.= b ^ {} by Def34
.= b by FINSEQ_1:47 ; :: thesis: verum

end;

then a is_a_unity_wrt H₂(D *+^ ) by BINOP_1:11;
hence the_unity_wrt the multF of (D *+^ ) = {} by BINOP_1:def 8; :: thesis: verum