let D be non empty set ; :: thesis: for F being non empty SubStr of D *+^ st {} is Element of F holds
( F is unital & the_unity_wrt the multF of F = {} )
let F be non empty SubStr of D *+^ ; :: thesis: ( {} is Element of F implies ( F is unital & the_unity_wrt the multF of F = {} ) )
the_unity_wrt H₂(D *+^ ) = {} by Th69;
hence ( {} is Element of F implies ( F is unital & the_unity_wrt the multF of F = {} ) ) by Th32; :: thesis: verum