theorem Th39: :: GR_FREE0:38

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q1, q2 being FinSequence of FreeAtoms G st [p,q1] in ReductionRel G & [p,q2] in ReductionRel G & q1 <> q2 & ( for s, t being FinSequence of FreeAtoms G
for i being Element of I
for f, g, h being Element of (G . i) holds
( not p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t or ( not ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) & not ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) ) holds
ex r, s, t being FinSequence of FreeAtoms G ex i, j being Element of I st
( ( p = (((r ^ <*[i,(1_ (G . i))]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (G . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (G . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t ) ) ) or ex g, h being Element of (G . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (G . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (G . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (G . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (G . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (G . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) )