let I be non empty set ; :: thesis: 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
let G be Group-like multMagma-Family of I; :: thesis: for p, q being FinSequence st [p,q] in ReductionRel G holds
len p = (len q) + 1
let p9, q9 be FinSequence; :: thesis: ( [p9,q9] in ReductionRel G implies len p9 = (len q9) + 1 )
assume A1: [p9,q9] in ReductionRel G ; :: thesis: len p9 = (len q9) + 1
then reconsider p = p9, q = q9 as FinSequence of FreeAtoms G by Th31;

per cases ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) by A1, Def3;

suppose ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) ; :: thesis: len p9 = (len q9) + 1

then consider s, t being FinSequence of FreeAtoms G, i being Element of I such that
A2: ( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) ;
thus len p9 = (len (s ^ <*[i,(1_ (G . i))]*>)) + (len t) by A2, FINSEQ_1:22
.= ((len s) + 1) + (len t) by FINSEQ_2:16
.= ((len s) + (len t)) + 1
.= (len q9) + 1 by A2, FINSEQ_1:22 ; :: thesis: verum

end;

suppose ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ; :: thesis: len p9 = (len q9) + 1

then consider s, t being FinSequence of FreeAtoms G, i being Element of I, g, h being Element of (G . i) such that
A3: ( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ;
thus len p9 = (len (s ^ <*[i,g],[i,h]*>)) + (len t) by A3, FINSEQ_1:22
.= ((len s) + (len <*[i,g],[i,h]*>)) + (len t) by FINSEQ_1:22
.= ((len s) + (1 + 1)) + (len t) by FINSEQ_1:44
.= (((len s) + 1) + (len t)) + 1
.= ((len (s ^ <*[i,(g * h)]*>)) + (len t)) + 1 by FINSEQ_2:16
.= (len q9) + 1 by A3, FINSEQ_1:22 ; :: thesis: verum

end;

end;