theorem Th35: :: GR_FREE0:34

for I being non empty set
for G being Group-like multMagma-Family of I
for p, q being FinSequence st [p,q] in ReductionRel G holds
len p = (len q) + 1