let D be non empty set ; :: thesis: for F being non empty unital SubStr of D *+^ holds the_unity_wrt the multF of F = {}
let F be non empty unital SubStr of D *+^ ; :: thesis: the_unity_wrt the multF of F = {}
set p = the_unity_wrt H₂(F);
reconsider q = the_unity_wrt H₂(F) as Element of F ;
A1: H₂(F) is having_a_unity by Def10;
q ^ {} = the_unity_wrt H₂(F) by FINSEQ_1:47
.= (the_unity_wrt H₂(F)) [*] (the_unity_wrt H₂(F)) by A1, SETWISEO:23
.= q ^ q by Th72 ;
hence the_unity_wrt the multF of F = {} by FINSEQ_1:46; :: thesis: verum