per cases ( not I is empty or I is empty ) ;

suppose A1: not I is empty ; :: thesis: EqCl (ReductionRel H) is compatible

now :: thesis: for v, v9, w, w9 being Element of ((FreeAtoms H) *+^+<0>) st v in Class ((EqCl (ReductionRel H)),v9) & w in Class ((EqCl (ReductionRel H)),w9) holds
v * w in Class ((EqCl (ReductionRel H)),(v9 * w9))

let v, v9, w, w9 be Element of ((FreeAtoms H) *+^+<0>); :: thesis: ( v in Class ((EqCl (ReductionRel H)),v9) & w in Class ((EqCl (ReductionRel H)),w9) implies v * w in Class ((EqCl (ReductionRel H)),(v9 * w9)) )
set S = the carrier of ((FreeAtoms H) *+^+<0>);
( v in the carrier of ((FreeAtoms H) *+^+<0>) & v9 in the carrier of ((FreeAtoms H) *+^+<0>) & w in the carrier of ((FreeAtoms H) *+^+<0>) & w9 in the carrier of ((FreeAtoms H) *+^+<0>) ) ;
then ( v in (FreeAtoms H) * & v9 in (FreeAtoms H) * & w in (FreeAtoms H) * & w9 in (FreeAtoms H) * ) by MONOID_0:61;
then reconsider q1 = v, p1 = v9, q2 = w, p2 = w9 as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
set R = EqCl (ReductionRel H);
assume ( v in Class ((EqCl (ReductionRel H)),v9) & w in Class ((EqCl (ReductionRel H)),w9) ) ; :: thesis: v * w in Class ((EqCl (ReductionRel H)),(v9 * w9))
then ( [v9,v] in EqCl (ReductionRel H) & [w9,w] in EqCl (ReductionRel H) ) by EQREL_1:18;
then ( p1,q1 are_convertible_wrt ReductionRel H & p2,q2 are_convertible_wrt ReductionRel H ) by MSUALG_6:41;
then p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H by A1, Th43;
then v9 * w9,q1 ^ q2 are_convertible_wrt ReductionRel H by MONOID_0:62;
then v9 * w9,v * w are_convertible_wrt ReductionRel H by MONOID_0:62;
then [(v9 * w9),(v * w)] in EqCl (ReductionRel H) by MSUALG_6:41;
hence v * w in Class ((EqCl (ReductionRel H)),(v9 * w9)) by EQREL_1:18; :: thesis: verum

end;

hence EqCl (ReductionRel H) is compatible by ALGSTR_4:def 3; :: thesis: verum

end;

suppose I is empty ; :: thesis: EqCl (ReductionRel H) is compatible

then H is empty ;
then FreeAtoms H is empty ;
hence EqCl (ReductionRel H) is compatible ; :: thesis: verum

end;

end;