consider p being Element of ((FreeAtoms H) *+^+<0>) such that
A1: s = Class ((EqCl (ReductionRel H)),p) by EQREL_1:36;
A2: p in the carrier of ((FreeAtoms H) *+^+<0>) ;
set q = nf (p,(ReductionRel H));
nf (p,(ReductionRel H)) is_a_normal_form_of p, ReductionRel H by REWRITE1:54;
then A3: ( nf (p,(ReductionRel H)) is_a_normal_form_wrt ReductionRel H & ReductionRel H reduces p, nf (p,(ReductionRel H)) ) by REWRITE1:def 6;
p in (FreeAtoms H) * by A2, MONOID_0:61;
then p in field (ReductionRel H) by Th30;
then nf (p,(ReductionRel H)) in field (ReductionRel H) by A3, REWRITE1:19;
then A4: nf (p,(ReductionRel H)) in (FreeAtoms H) * by Th30;
then reconsider q = nf (p,(ReductionRel H)) as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
take q ; :: thesis: ( q in s & q is_a_normal_form_wrt ReductionRel H )
A5: q in the carrier of ((FreeAtoms H) *+^+<0>) by A4, MONOID_0:61;
p,q are_convertible_wrt ReductionRel H by A3, REWRITE1:25;
then [p,q] in EqCl (ReductionRel H) by A5, MSUALG_6:41;
then s = Class ((EqCl (ReductionRel H)),q) by A1, EQREL_1:35;
hence ( q in s & q is_a_normal_form_wrt ReductionRel H ) by A3, A5, EQREL_1:20; :: thesis: verum