let D be 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 :: thesis: for b being Element of (D *+^) holds
( H₂(D *+^ ) . (a,b) = b & H₂(D *+^ ) . (b,a) = b )

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:34 ; :: thesis: H₂(D *+^ ) . (b,a) = b
thus H₂(D *+^ ) . (b,a) = b [*] a
.= b ^ {} by Def34
.= b by FINSEQ_1:34 ; :: thesis: verum

end;

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