let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I holds factorization (1_ (FreeProduct H)) = {}
let H be Group-like associative multMagma-Family of I; :: thesis: factorization (1_ (FreeProduct H)) = {}
thus factorization (1_ (FreeProduct H)) = (uncurry (injection H)) * {} by Th62
.= {} ; :: thesis: verum