let D be 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 ;
q ^ {} = the_unity_wrt H₂(F) by FINSEQ_1:34
.= (the_unity_wrt H₂(F)) [*] (the_unity_wrt H₂(F)) by SETWISEO:15
.= q ^ q by Th63 ;
hence the_unity_wrt the multF of F = {} by FINSEQ_1:33; :: thesis: verum