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) = 1 holds
ex i being Element of I ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] )
let H be Group-like associative multMagma-Family of I; :: thesis: for s being Element of (FreeProduct H) st len (nf s) = 1 holds
ex i being Element of I ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] )
let s be Element of (FreeProduct H); :: thesis: ( len (nf s) = 1 implies ex i being Element of I ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] ) )
assume A1: len (nf s) = 1 ; :: thesis: ex i being Element of I ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] )
then 1 in dom (nf s) by FINSEQ_3:25;
then (nf s) . 1 in rng (nf s) by FUNCT_1:3;
then reconsider z = (nf s) . 1 as Element of FreeAtoms H ;
consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
x in dom H by A2, Th7;
then reconsider i = x as Element of I ;
reconsider g = y as Element of (H . i) by A2, Th9;
take i ; :: thesis: ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] )
take g ; :: thesis: ( g <> 1_ (H . i) & s = [*i,g*] )
A3: nf s = <*[i,g]*> by A1, A2, FINSEQ_1:40;
thus g <> 1_ (H . i) :: thesis: s = [*i,g*]

proof

assume g = 1_ (H . i) ; :: thesis: contradiction
then A4: <*[i,(1_ (H . i))]*> is_a_normal_form_wrt ReductionRel H by A3, Def7;
[<*[i,(1_ (H . i))]*>,{}] in ReductionRel H by Th29;
hence contradiction by A4, REWRITE1:def 5; :: thesis: verum

end;

consider p being Element of ((FreeAtoms H) *+^+<0>) such that
A5: s = Class ((EqCl (ReductionRel H)),p) by EQREL_1:36;
<*[i,g]*> in s by A3, Def7;
hence s = [*i,g*] by A5, EQREL_1:23; :: thesis: verum