let I be non empty set ; :: thesis: for i, j being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i)
for h being Element of (H . j) holds
( <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )
let i, j be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I
for g being Element of (H . i)
for h being Element of (H . j) holds
( <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )
let H be Group-like associative multMagma-Family of I; :: thesis: for g being Element of (H . i)
for h being Element of (H . j) holds
( <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )
let g be Element of (H . i); :: thesis: for h being Element of (H . j) holds
( <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )
let h be Element of (H . j); :: thesis: ( <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )
( [i,g] in FreeAtoms H & [j,h] in FreeAtoms H ) by Th9;
then reconsider s1 = <*[i,g]*>, s2 = <*[j,h]*> as FinSequence of FreeAtoms H by FINSEQ_1:74;

hereby :: thesis: ( ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) implies <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H )

assume <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H ; :: thesis: ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) )
then s1,s2 are_convergent_wrt ReductionRel H by REWRITE1:def 23;
then consider c being object such that
A1: ReductionRel H reduces <*[i,g]*>,c and
A2: ReductionRel H reduces <*[j,h]*>,c by REWRITE1:def 7;

per cases ( c = s1 or c <> s1 ) ;

suppose A3: c = s1 ; :: thesis: ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) )

( len s1 = 1 & len s2 = 1 ) by FINSEQ_1:40;
then [i,g] = [j,h] by A2, A3, Th36, FINSEQ_1:76;
hence ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) by XTUPLE_0:1; :: thesis: verum

end;

suppose A4: c <> s1 ; :: thesis: ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) )

then c in field (ReductionRel H) by A1, REWRITE1:18;
then c in (FreeAtoms H) * by Th30;
then reconsider c = c as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
len c < len s1 by A1, A4, Th36;
then len c < 1 by FINSEQ_1:40;
then c <> s2 by FINSEQ_1:40;
hence ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) by A1, A2, A4, Th38, REWRITE1:33; :: thesis: verum

end;

end;

end;

assume ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) ; :: thesis: <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H

per cases then ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) ;

suppose ( g = 1_ (H . i) & h = 1_ (H . j) ) ; :: thesis: <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H

then ( [s1,{}] in ReductionRel H & [s2,{}] in ReductionRel H ) by Th29;
then A5: ( s1, {} are_convertible_wrt ReductionRel H & s2, {} are_convertible_wrt ReductionRel H ) by REWRITE1:29;
then {} ,s2 are_convertible_wrt ReductionRel H by REWRITE1:31;
hence <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H by A5, REWRITE1:30; :: thesis: verum

end;

suppose ( i = j & g = h ) ; :: thesis: <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H

hence <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H by REWRITE1:26; :: thesis: verum

end;

end;