let q1, q2 be FinSequence of FreeAtoms H; :: thesis: ( q1 in s & q1 is_a_normal_form_wrt ReductionRel H & q2 in s & q2 is_a_normal_form_wrt ReductionRel H implies q1 = q2 )
assume that
A6: ( q1 in s & q1 is_a_normal_form_wrt ReductionRel H ) and
A7: ( q2 in s & q2 is_a_normal_form_wrt ReductionRel H ) ; :: thesis: q1 = q2
consider p being Element of ((FreeAtoms H) *+^+<0>) such that
A8: s = Class ((EqCl (ReductionRel H)),p) by EQREL_1:36;
( q1 in (FreeAtoms H) * & q2 in (FreeAtoms H) * ) by FINSEQ_1:def 11;
then A9: ( q1 in the carrier of ((FreeAtoms H) *+^+<0>) & q2 in the carrier of ((FreeAtoms H) *+^+<0>) ) by MONOID_0:61;
[q1,q2] in EqCl (ReductionRel H) by A6, A7, A8, EQREL_1:22;
hence q1 = q2 by A6, A7, A9, MSUALG_6:41, REWRITE1:def 19; :: thesis: verum