let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I holds nf (1_ (FreeProduct H)) = {}
let H be Group-like associative multMagma-Family of I; :: thesis: nf (1_ (FreeProduct H)) = {}
set p = <*> (FreeAtoms H);
1_ (FreeProduct H) = Class ((EqCl (ReductionRel H)),(<*> (FreeAtoms H))) by Th45;
hence nf (1_ (FreeProduct H)) = nf ((<*> (FreeAtoms H)),(ReductionRel H)) by Th59
.= {} by Th37, MSAFREE4:17 ;
:: thesis: verum