let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I
for g, h being Element of (H . i) holds [*i,g*] * [*i,h*] = [*i,(g * h)*]
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I
for g, h being Element of (H . i) holds [*i,g*] * [*i,h*] = [*i,(g * h)*]
let H be Group-like associative multMagma-Family of I; :: thesis: for g, h being Element of (H . i) holds [*i,g*] * [*i,h*] = [*i,(g * h)*]
let g, h be Element of (H . i); :: thesis: [*i,g*] * [*i,h*] = [*i,(g * h)*]
set R = EqCl (ReductionRel H);
( [i,g] in FreeAtoms H & [i,h] in FreeAtoms H ) by Th9;
then reconsider s1 = <*[i,g]*>, s2 = <*[i,h]*> as FinSequence of FreeAtoms H by FINSEQ_1:74;
s1 ^ s2 in (FreeAtoms H) * ;
then A1: s1 ^ s2 in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
A2: [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel H by Th27;
ReductionRel H c= EqCl (ReductionRel H) by MSUALG_5:def 1;
then [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in EqCl (ReductionRel H) by A2;
then A3: [(s1 ^ s2),<*[i,(g * h)]*>] in EqCl (ReductionRel H) by FINSEQ_1:def 9;
thus [*i,g*] * [*i,h*] = Class ((EqCl (ReductionRel H)),(s1 ^ s2)) by Th47
.= [*i,(g * h)*] by A1, A3, EQREL_1:35 ; :: thesis: verum