let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) st len (nf s) = 0 holds
s = 1_ (FreeProduct H)
let H be Group-like associative multMagma-Family of I; :: thesis: for s being Element of (FreeProduct H) st len (nf s) = 0 holds
s = 1_ (FreeProduct H)
let s be Element of (FreeProduct H); :: thesis: ( len (nf s) = 0 implies s = 1_ (FreeProduct H) )
assume len (nf s) = 0 ; :: thesis: s = 1_ (FreeProduct H)
then nf s = {} ;
then A1: {} in s by Def7;
consider x being Element of ((FreeAtoms H) *+^+<0>) such that
A2: s = Class ((EqCl (ReductionRel H)),x) by EQREL_1:36;
thus s = Class ((EqCl (ReductionRel H)),{}) by A1, A2, EQREL_1:23
.= 1_ (FreeProduct H) by Th45 ; :: thesis: verum