:: deftheorem Def2 defines ReductionRel GR_FREE0:def 2 :
for I being set
for G being Group-like multMagma-Family of I
for b₃ being Relation of ((FreeAtoms G) *+^+<0>) holds
( b₃ = ReductionRel G iff ( ( I is empty implies b₃ = {} ) & ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in b₃ iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) ) );