let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I holds [<*[i,(1_ (G . i))]*>,{}] in ReductionRel G
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I holds [<*[i,(1_ (G . i))]*>,{}] in ReductionRel G
let G be Group-like multMagma-Family of I; :: thesis: [<*[i,(1_ (G . i))]*>,{}] in ReductionRel G
set p = <*> (FreeAtoms G);
[(((<*> (FreeAtoms G)) ^ <*[i,(1_ (G . i))]*>) ^ (<*> (FreeAtoms G))),((<*> (FreeAtoms G)) ^ (<*> (FreeAtoms G)))] = [(<*[i,(1_ (G . i))]*> ^ (<*> (FreeAtoms G))),((<*> (FreeAtoms G)) ^ (<*> (FreeAtoms G)))] by FINSEQ_1:34
.= [<*[i,(1_ (G . i))]*>,((<*> (FreeAtoms G)) ^ (<*> (FreeAtoms G)))] by FINSEQ_1:34
.= [<*[i,(1_ (G . i))]*>,{}] ;
hence [<*[i,(1_ (G . i))]*>,{}] in ReductionRel G by Th28; :: thesis: verum