let D be non empty set ; :: thesis: the_unity_wrt the multF of (D *+^ ) = {}
set N = D *+^ ;
set f = H₂(D *+^ );
( H₁(D *+^ ) = D * & {} = <*> D ) by Def34;
then reconsider a = {} as Element of (D *+^ ) by 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