the carrier of (FreeProduct H) = {(1_ (FreeProduct H))} by Th46;
hence FreeProduct H is trivial ; :: thesis: verum