let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for p being FinSequence of FreeAtoms H
for s being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) holds
nf s = nf (p,(ReductionRel H))
let H be Group-like associative multMagma-Family of I; :: thesis: for p being FinSequence of FreeAtoms H
for s being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) holds
nf s = nf (p,(ReductionRel H))
let p be FinSequence of FreeAtoms H; :: thesis: for s being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) holds
nf s = nf (p,(ReductionRel H))
let s be Element of (FreeProduct H); :: thesis: ( s = Class ((EqCl (ReductionRel H)),p) implies nf s = nf (p,(ReductionRel H)) )
assume A1: s = Class ((EqCl (ReductionRel H)),p) ; :: thesis: nf s = nf (p,(ReductionRel H))
set q = nf (p,(ReductionRel H));
nf (p,(ReductionRel H)) is_a_normal_form_of p, ReductionRel H by REWRITE1:54;
then A2: ( nf (p,(ReductionRel H)) is_a_normal_form_wrt ReductionRel H & ReductionRel H reduces p, nf (p,(ReductionRel H)) ) by REWRITE1:def 6;
A3: p in (FreeAtoms H) * by FINSEQ_1:def 11;
then p in field (ReductionRel H) by Th30;
then nf (p,(ReductionRel H)) in field (ReductionRel H) by A2, REWRITE1:19;
then A4: nf (p,(ReductionRel H)) in (FreeAtoms H) * by Th30;
then A5: nf (p,(ReductionRel H)) in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
A6: p in the carrier of ((FreeAtoms H) *+^+<0>) by A3, MONOID_0:61;
p, nf (p,(ReductionRel H)) are_convertible_wrt ReductionRel H by A2, REWRITE1:25;
then [p,(nf (p,(ReductionRel H)))] in EqCl (ReductionRel H) by A5, A6, MSUALG_6:41;
then A7: nf (p,(ReductionRel H)) in s by A1, EQREL_1:18;
nf (p,(ReductionRel H)) is FinSequence of FreeAtoms H by A4, FINSEQ_1:def 11;
hence nf s = nf (p,(ReductionRel H)) by A2, A7, Def7; :: thesis: verum