let D be non empty set ; :: thesis: the_unity_wrt the multF of (D *+^) = {}
set N = D *+^ ;
set f = H2(D *+^ );
( H1(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
( H2(D *+^ ) . (a,b) = b & H2(D *+^ ) . (b,a) = b )
let b be Element of (D *+^); :: thesis: ( H2(D *+^ ) . (a,b) = b & H2(D *+^ ) . (b,a) = b )
thus H2(D *+^ ) . (a,b) = a [*] b
.= {} ^ b by Def34
.= b by FINSEQ_1:34 ; :: thesis: H2(D *+^ ) . (b,a) = b
thus H2(D *+^ ) . (b,a) = b [*] a
.= b ^ {} by Def34
.= b by FINSEQ_1:34 ; :: thesis: verum
end;
then a is_a_unity_wrt H2(D *+^ ) by BINOP_1:3;
hence the_unity_wrt the multF of (D *+^) = {} by BINOP_1:def 8; :: thesis: verum