let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for k being Nat
for s, t being Element of (FreeProduct H) st t = Class ((EqCl (ReductionRel H)),((nf s) | k)) holds
nf t = (nf s) | k
let H be Group-like associative multMagma-Family of I; :: thesis: for k being Nat
for s, t being Element of (FreeProduct H) st t = Class ((EqCl (ReductionRel H)),((nf s) | k)) holds
nf t = (nf s) | k
let k be Nat; :: thesis: for s, t being Element of (FreeProduct H) st t = Class ((EqCl (ReductionRel H)),((nf s) | k)) holds
nf t = (nf s) | k
let s, t be Element of (FreeProduct H); :: thesis: ( t = Class ((EqCl (ReductionRel H)),((nf s) | k)) implies nf t = (nf s) | k )
assume A1: t = Class ((EqCl (ReductionRel H)),((nf s) | k)) ; :: thesis: nf t = (nf s) | k
(nf s) | k in (FreeAtoms H) * by FINSEQ_1:def 11;
then (nf s) | k is Element of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
then A2: (nf s) | k in t by A1, EQREL_1:23;
(nf s) | k is_a_normal_form_wrt ReductionRel H

proof

assume not (nf s) | k is_a_normal_form_wrt ReductionRel H ; :: thesis: contradiction
then consider b being object such that
A3: [((nf s) | k),b] in ReductionRel H by REWRITE1:def 5;
b in rng (ReductionRel H) by A3, XTUPLE_0:def 13;
then b in the carrier of ((FreeAtoms H) *+^+<0>) ;
then b in (FreeAtoms H) * by MONOID_0:61;
then reconsider b = b as FinSequence of FreeAtoms H by FINSEQ_1:def 11;

per cases ( ex r, u being FinSequence of FreeAtoms H ex i being Element of I st
( (nf s) | k = (r ^ <*[i,(1_ (H . i))]*>) ^ u & b = r ^ u ) or ex r, u being FinSequence of FreeAtoms H ex i being Element of I ex g, h being Element of (H . i) st
( (nf s) | k = (r ^ <*[i,g],[i,h]*>) ^ u & b = (r ^ <*[i,(g * h)]*>) ^ u ) ) by A3, Def3;

suppose ex r, u being FinSequence of FreeAtoms H ex i being Element of I st
( (nf s) | k = (r ^ <*[i,(1_ (H . i))]*>) ^ u & b = r ^ u ) ; :: thesis: contradiction

then consider r, u being FinSequence of FreeAtoms H, i being Element of I such that
A4: ( (nf s) | k = (r ^ <*[i,(1_ (H . i))]*>) ^ u & b = r ^ u ) ;
A5: nf s = ((r ^ <*[i,(1_ (H . i))]*>) ^ u) ^ ((nf s) /^ k) by A4, RFINSEQ:8
.= (r ^ <*[i,(1_ (H . i))]*>) ^ (u ^ ((nf s) /^ k)) by FINSEQ_1:32 ;
set b9 = r ^ (u ^ ((nf s) /^ k));
reconsider b9 = r ^ (u ^ ((nf s) /^ k)) as FinSequence of FreeAtoms H ;
[(nf s),b9] in ReductionRel H by A5, Def3;
hence contradiction by Def7, REWRITE1:def 5; :: thesis: verum

end;

suppose ex r, u being FinSequence of FreeAtoms H ex i being Element of I ex g, h being Element of (H . i) st
( (nf s) | k = (r ^ <*[i,g],[i,h]*>) ^ u & b = (r ^ <*[i,(g * h)]*>) ^ u ) ; :: thesis: contradiction

then consider r, u being FinSequence of FreeAtoms H, i being Element of I, g, h being Element of (H . i) such that
A6: ( (nf s) | k = (r ^ <*[i,g],[i,h]*>) ^ u & b = (r ^ <*[i,(g * h)]*>) ^ u ) ;
A7: nf s = ((r ^ <*[i,g],[i,h]*>) ^ u) ^ ((nf s) /^ k) by A6, RFINSEQ:8
.= (r ^ <*[i,g],[i,h]*>) ^ (u ^ ((nf s) /^ k)) by FINSEQ_1:32 ;
set b9 = (r ^ <*[i,(g * h)]*>) ^ (u ^ ((nf s) /^ k));
r ^ <*[i,(g * h)]*> is FinSequence of FreeAtoms H by A6, FINSEQ_1:36;
then reconsider b9 = (r ^ <*[i,(g * h)]*>) ^ (u ^ ((nf s) /^ k)) as FinSequence of FreeAtoms H by FINSEQ_1:75;
[(nf s),b9] in ReductionRel H by A7, Def3;
hence contradiction by Def7, REWRITE1:def 5; :: thesis: verum

end;

end;

end;

hence nf t = (nf s) | k by A2, Def7; :: thesis: verum