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*] 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*] 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*] 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*] 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*] iff ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) )
[i,g] in FreeAtoms H by Th9;
then <*[i,g]*> is FinSequence of FreeAtoms H by FINSEQ_1:74;
then <*[i,g]*> in (FreeAtoms H) * by FINSEQ_1:def 11;
then A1: <*[i,g]*> in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
[j,h] in FreeAtoms H by Th9;
then <*[j,h]*> is FinSequence of FreeAtoms H by FINSEQ_1:74;
then <*[j,h]*> in (FreeAtoms H) * by FINSEQ_1:def 11;
then A2: <*[j,h]*> in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;

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

assume [*i,g*] = [*j,h*] ; :: thesis: ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) )
then [<*[i,g]*>,<*[j,h]*>] in EqCl (ReductionRel H) by A1, EQREL_1:35;
then <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H by A1, A2, MSUALG_6:41;
hence ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) by Th40; :: thesis: verum

end;

assume ( ( g = 1_ (H . i) & h = 1_ (H . j) ) or ( i = j & g = h ) ) ; :: thesis: [*i,g*] = [*j,h*]
then <*[i,g]*>,<*[j,h]*> are_convertible_wrt ReductionRel H by Th40;
then [<*[i,g]*>,<*[j,h]*>] in EqCl (ReductionRel H) by A1, A2, MSUALG_6:41;
hence [*i,g*] = [*j,h*] by A1, EQREL_1:35; :: thesis: verum