let I be non empty set ; :: thesis: 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 ) ) ) ) )
let G be Group-like multMagma-Family of I; :: thesis: 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 ) ) ) ) )
let p, q1, q2 be FinSequence of FreeAtoms G; :: thesis: ( [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 ) ) ) ) implies 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 ) ) ) ) ) )
assume A1: ( [p,q1] in ReductionRel G & [p,q2] in ReductionRel G & q1 <> q2 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

per cases then ( ex s1, t1 being FinSequence of FreeAtoms G ex i1 being Element of I st
( p = (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ t1 & q1 = s1 ^ t1 ) or ex s1, t1 being FinSequence of FreeAtoms G ex i1 being Element of I ex g1, h1 being Element of (G . i1) st
( p = (s1 ^ <*[i1,g1],[i1,h1]*>) ^ t1 & q1 = (s1 ^ <*[i1,(g1 * h1)]*>) ^ t1 ) ) by Def3;

suppose ex s1, t1 being FinSequence of FreeAtoms G ex i1 being Element of I st
( p = (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ t1 & q1 = s1 ^ t1 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then consider s1, t1 being FinSequence of FreeAtoms G, i1 being Element of I such that
A2: ( p = (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ t1 & q1 = s1 ^ t1 ) ;

per cases ( ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I st
( p = (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ t2 & q2 = s2 ^ t2 ) or ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I ex g2, h2 being Element of (G . i2) st
( p = (s2 ^ <*[i2,g2],[i2,h2]*>) ^ t2 & q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ t2 ) ) by A1, Def3;

suppose ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I st
( p = (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ t2 & q2 = s2 ^ t2 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then consider s2, t2 being FinSequence of FreeAtoms G, i2 being Element of I such that
A3: ( p = (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ t2 & q2 = s2 ^ t2 ) ;
len s1 <> len s2

proof

assume A4: len s1 = len s2 ; :: thesis: contradiction
len <*[i1,(1_ (G . i1))]*> = 1 by FINSEQ_1:39
.= len <*[i2,(1_ (G . i2))]*> by FINSEQ_1:39 ;
then ( s1 = s2 & t1 = t2 ) by A2, A3, A4, Lm2;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

per cases then ( len s1 < len s2 or len s2 < len s1 ) by XXREAL_0:1;

suppose len s1 < len s2 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then (len s1) + 1 <= len s2 by NAT_1:13;
then A5: len (s1 ^ <*[i1,(1_ (G . i1))]*>) <= len s2 by FINSEQ_2:16;
p = s2 ^ (<*[i2,(1_ (G . i2))]*> ^ t2) by A3, FINSEQ_1:32;
then consider s being FinSequence such that
A6: (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ s = s2 by A2, A5, FINSEQ_1:47;
set r = s1;
set t = t2;
reconsider s = s as FinSequence of FreeAtoms G by A6, FINSEQ_1:36;
p = (((s1 ^ <*[i1,(1_ (G . i1))]*>) ^ s) ^ <*[i2,(1_ (G . i2))]*>) ^ t2 by A3, A6;
then p = ((s1 ^ <*[i1,(1_ (G . i1))]*>) ^ s) ^ (<*[i2,(1_ (G . i2))]*> ^ t2) by FINSEQ_1:32
.= (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ (s ^ (<*[i2,(1_ (G . i2))]*> ^ t2)) by FINSEQ_1:32
.= (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ ((s ^ <*[i2,(1_ (G . i2))]*>) ^ t2) by FINSEQ_1:32 ;
then q1 = s1 ^ ((s ^ <*[i2,(1_ (G . i2))]*>) ^ t2) by A2, FINSEQ_1:33
.= s1 ^ (s ^ (<*[i2,(1_ (G . i2))]*> ^ t2)) by FINSEQ_1:32
.= (s1 ^ s) ^ (<*[i2,(1_ (G . i2))]*> ^ t2) by FINSEQ_1:32
.= ((s1 ^ s) ^ <*[i2,(1_ (G . i2))]*>) ^ t2 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A3, A6; :: thesis: verum

end;

suppose len s2 < len s1 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then (len s2) + 1 <= len s1 by NAT_1:13;
then A7: len (s2 ^ <*[i2,(1_ (G . i2))]*>) <= len s1 by FINSEQ_2:16;
p = s1 ^ (<*[i1,(1_ (G . i1))]*> ^ t1) by A2, FINSEQ_1:32;
then consider s being FinSequence such that
A8: (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ s = s1 by A3, A7, FINSEQ_1:47;
set r = s2;
set t = t1;
reconsider s = s as FinSequence of FreeAtoms G by A8, FINSEQ_1:36;
p = (((s2 ^ <*[i2,(1_ (G . i2))]*>) ^ s) ^ <*[i1,(1_ (G . i1))]*>) ^ t1 by A2, A8;
then p = ((s2 ^ <*[i2,(1_ (G . i2))]*>) ^ s) ^ (<*[i1,(1_ (G . i1))]*> ^ t1) by FINSEQ_1:32
.= (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ (s ^ (<*[i1,(1_ (G . i1))]*> ^ t1)) by FINSEQ_1:32
.= (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ ((s ^ <*[i1,(1_ (G . i1))]*>) ^ t1) by FINSEQ_1:32 ;
then q2 = s2 ^ ((s ^ <*[i1,(1_ (G . i1))]*>) ^ t1) by A3, FINSEQ_1:33
.= s2 ^ (s ^ (<*[i1,(1_ (G . i1))]*> ^ t1)) by FINSEQ_1:32
.= (s2 ^ s) ^ (<*[i1,(1_ (G . i1))]*> ^ t1) by FINSEQ_1:32
.= ((s2 ^ s) ^ <*[i1,(1_ (G . i1))]*>) ^ t1 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A2, A8; :: thesis: verum

end;

end;

end;

suppose ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I ex g2, h2 being Element of (G . i2) st
( p = (s2 ^ <*[i2,g2],[i2,h2]*>) ^ t2 & q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ t2 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then consider s2, t2 being FinSequence of FreeAtoms G, i2 being Element of I, g2, h2 being Element of (G . i2) such that
A9: ( p = (s2 ^ <*[i2,g2],[i2,h2]*>) ^ t2 & q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ t2 ) ;
len s1 <> len s2

proof

assume A10: len s1 = len s2 ; :: thesis: contradiction
A11: p = (s2 ^ (<*[i2,g2]*> ^ <*[i2,h2]*>)) ^ t2 by A9, FINSEQ_1:def 9
.= s2 ^ ((<*[i2,g2]*> ^ <*[i2,h2]*>) ^ t2) by FINSEQ_1:32
.= s2 ^ (<*[i2,g2]*> ^ (<*[i2,h2]*> ^ t2)) by FINSEQ_1:32
.= (s2 ^ <*[i2,g2]*>) ^ (<*[i2,h2]*> ^ t2) by FINSEQ_1:32 ;
len <*[i1,(1_ (G . i1))]*> = 1 by FINSEQ_1:39
.= len <*[i2,g2]*> by FINSEQ_1:39 ;
then A12: ( s1 = s2 & <*[i1,(1_ (G . i1))]*> = <*[i2,g2]*> & t1 = <*[i2,h2]*> ^ t2 ) by A2, A10, A11, Lm2;
then [i1,(1_ (G . i1))] = [i2,g2] by FINSEQ_1:76;
then ( i1 = i2 & 1_ (G . i1) = g2 ) by XTUPLE_0:1;
then h2 = g2 * h2 by GROUP_1:def 4;
hence contradiction by A1, A9, A2, A12, FINSEQ_1:32; :: thesis: verum

end;

per cases then ( len s1 < len s2 or len s2 < len s1 ) by XXREAL_0:1;

suppose len s1 < len s2 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then (len s1) + 1 <= len s2 by NAT_1:13;
then A13: len (s1 ^ <*[i1,(1_ (G . i1))]*>) <= len s2 by FINSEQ_2:16;
p = s2 ^ (<*[i2,g2],[i2,h2]*> ^ t2) by A9, FINSEQ_1:32;
then consider s being FinSequence such that
A14: (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ s = s2 by A2, A13, FINSEQ_1:47;
set r = s1;
set t = t2;
reconsider s = s as FinSequence of FreeAtoms G by A14, FINSEQ_1:36;
p = (((s1 ^ <*[i1,(1_ (G . i1))]*>) ^ s) ^ <*[i2,g2],[i2,h2]*>) ^ t2 by A9, A14;
then p = ((s1 ^ <*[i1,(1_ (G . i1))]*>) ^ s) ^ (<*[i2,g2],[i2,h2]*> ^ t2) by FINSEQ_1:32
.= (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ (s ^ (<*[i2,g2],[i2,h2]*> ^ t2)) by FINSEQ_1:32
.= (s1 ^ <*[i1,(1_ (G . i1))]*>) ^ ((s ^ <*[i2,g2],[i2,h2]*>) ^ t2) by FINSEQ_1:32 ;
then q1 = s1 ^ ((s ^ <*[i2,g2],[i2,h2]*>) ^ t2) by A2, FINSEQ_1:33
.= s1 ^ (s ^ (<*[i2,g2],[i2,h2]*> ^ t2)) by FINSEQ_1:32
.= (s1 ^ s) ^ (<*[i2,g2],[i2,h2]*> ^ t2) by FINSEQ_1:32
.= ((s1 ^ s) ^ <*[i2,g2],[i2,h2]*>) ^ t2 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A9, A14; :: thesis: verum

end;

suppose A15: len s2 < len s1 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

(len s2) + 1 <> len s1

proof

assume (len s2) + 1 = len s1 ; :: thesis: contradiction
then A16: len (s2 ^ <*[i2,g2]*>) = len s1 by FINSEQ_2:16;
A17: p = (s2 ^ (<*[i2,g2]*> ^ <*[i2,h2]*>)) ^ t2 by A9, FINSEQ_1:def 9
.= ((s2 ^ <*[i2,g2]*>) ^ <*[i2,h2]*>) ^ t2 by FINSEQ_1:32 ;
len <*[i1,(1_ (G . i1))]*> = 1 by FINSEQ_1:39
.= len <*[i2,h2]*> by FINSEQ_1:39 ;
then A18: ( s1 = s2 ^ <*[i2,g2]*> & <*[i1,(1_ (G . i1))]*> = <*[i2,h2]*> & t1 = t2 ) by A2, A16, A17, Lm2;
then [i1,(1_ (G . i1))] = [i2,h2] by FINSEQ_1:76;
then ( i1 = i2 & 1_ (G . i1) = h2 ) by XTUPLE_0:1;
hence contradiction by A1, A9, A2, A18, GROUP_1:def 4; :: thesis: verum

end;

then ( (len s2) + 1 < len s1 or (len s2) + 1 > len s1 ) by XXREAL_0:1;
then ((len s2) + 1) + 1 < (len s1) + 1 by A15, NAT_1:13, XREAL_1:8;
then (len s2) + 2 <= len s1 by NAT_1:13;
then (len s2) + (len <*[i2,g2],[i2,h2]*>) <= len s1 by FINSEQ_1:44;
then A19: len (s2 ^ <*[i2,g2],[i2,h2]*>) <= len s1 by FINSEQ_1:22;
p = s1 ^ (<*[i1,(1_ (G . i1))]*> ^ t1) by A2, FINSEQ_1:32;
then consider s being FinSequence such that
A20: (s2 ^ <*[i2,g2],[i2,h2]*>) ^ s = s1 by A9, A19, FINSEQ_1:47;
set r = s2;
set t = t1;
reconsider s = s as FinSequence of FreeAtoms G by A20, FINSEQ_1:36;
p = (((s2 ^ <*[i2,g2],[i2,h2]*>) ^ s) ^ <*[i1,(1_ (G . i1))]*>) ^ t1 by A2, A20;
then p = ((s2 ^ <*[i2,g2],[i2,h2]*>) ^ s) ^ (<*[i1,(1_ (G . i1))]*> ^ t1) by FINSEQ_1:32
.= (s2 ^ <*[i2,g2],[i2,h2]*>) ^ (s ^ (<*[i1,(1_ (G . i1))]*> ^ t1)) by FINSEQ_1:32
.= (s2 ^ <*[i2,g2],[i2,h2]*>) ^ ((s ^ <*[i1,(1_ (G . i1))]*>) ^ t1) by FINSEQ_1:32 ;
then q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ ((s ^ <*[i1,(1_ (G . i1))]*>) ^ t1) by A9, FINSEQ_1:33
.= (s2 ^ <*[i2,(g2 * h2)]*>) ^ (s ^ (<*[i1,(1_ (G . i1))]*> ^ t1)) by FINSEQ_1:32
.= ((s2 ^ <*[i2,(g2 * h2)]*>) ^ s) ^ (<*[i1,(1_ (G . i1))]*> ^ t1) by FINSEQ_1:32
.= (((s2 ^ <*[i2,(g2 * h2)]*>) ^ s) ^ <*[i1,(1_ (G . i1))]*>) ^ t1 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A2, A20; :: thesis: verum

end;

end;

end;

end;

end;

suppose ex s1, t1 being FinSequence of FreeAtoms G ex i1 being Element of I ex g1, h1 being Element of (G . i1) st
( p = (s1 ^ <*[i1,g1],[i1,h1]*>) ^ t1 & q1 = (s1 ^ <*[i1,(g1 * h1)]*>) ^ t1 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then consider s1, t1 being FinSequence of FreeAtoms G, i1 being Element of I, g1, h1 being Element of (G . i1) such that
A21: ( p = (s1 ^ <*[i1,g1],[i1,h1]*>) ^ t1 & q1 = (s1 ^ <*[i1,(g1 * h1)]*>) ^ t1 ) ;

per cases ( ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I st
( p = (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ t2 & q2 = s2 ^ t2 ) or ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I ex g2, h2 being Element of (G . i2) st
( p = (s2 ^ <*[i2,g2],[i2,h2]*>) ^ t2 & q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ t2 ) ) by A1, Def3;

suppose ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I st
( p = (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ t2 & q2 = s2 ^ t2 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then consider s2, t2 being FinSequence of FreeAtoms G, i2 being Element of I such that
A22: ( p = (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ t2 & q2 = s2 ^ t2 ) ;
len s1 <> len s2

proof

assume A23: len s2 = len s1 ; :: thesis: contradiction
A24: p = (s1 ^ (<*[i1,g1]*> ^ <*[i1,h1]*>)) ^ t1 by A21, FINSEQ_1:def 9
.= s1 ^ ((<*[i1,g1]*> ^ <*[i1,h1]*>) ^ t1) by FINSEQ_1:32
.= s1 ^ (<*[i1,g1]*> ^ (<*[i1,h1]*> ^ t1)) by FINSEQ_1:32
.= (s1 ^ <*[i1,g1]*>) ^ (<*[i1,h1]*> ^ t1) by FINSEQ_1:32 ;
len <*[i2,(1_ (G . i2))]*> = 1 by FINSEQ_1:39
.= len <*[i1,g1]*> by FINSEQ_1:39 ;
then A25: ( s2 = s1 & <*[i2,(1_ (G . i2))]*> = <*[i1,g1]*> & t2 = <*[i1,h1]*> ^ t1 ) by A22, A23, A24, Lm2;
then [i2,(1_ (G . i2))] = [i1,g1] by FINSEQ_1:76;
then ( i2 = i1 & 1_ (G . i2) = g1 ) by XTUPLE_0:1;
then h1 = g1 * h1 by GROUP_1:def 4;
hence contradiction by A1, A21, A22, A25, FINSEQ_1:32; :: thesis: verum

end;

per cases then ( len s2 < len s1 or len s1 < len s2 ) by XXREAL_0:1;

suppose len s2 < len s1 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then (len s2) + 1 <= len s1 by NAT_1:13;
then A26: len (s2 ^ <*[i2,(1_ (G . i2))]*>) <= len s1 by FINSEQ_2:16;
p = s1 ^ (<*[i1,g1],[i1,h1]*> ^ t1) by A21, FINSEQ_1:32;
then consider s being FinSequence such that
A27: (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ s = s1 by A22, A26, FINSEQ_1:47;
set r = s2;
set t = t1;
reconsider s = s as FinSequence of FreeAtoms G by A27, FINSEQ_1:36;
p = (((s2 ^ <*[i2,(1_ (G . i2))]*>) ^ s) ^ <*[i1,g1],[i1,h1]*>) ^ t1 by A21, A27;
then p = ((s2 ^ <*[i2,(1_ (G . i2))]*>) ^ s) ^ (<*[i1,g1],[i1,h1]*> ^ t1) by FINSEQ_1:32
.= (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ (s ^ (<*[i1,g1],[i1,h1]*> ^ t1)) by FINSEQ_1:32
.= (s2 ^ <*[i2,(1_ (G . i2))]*>) ^ ((s ^ <*[i1,g1],[i1,h1]*>) ^ t1) by FINSEQ_1:32 ;
then q2 = s2 ^ ((s ^ <*[i1,g1],[i1,h1]*>) ^ t1) by A22, FINSEQ_1:33
.= s2 ^ (s ^ (<*[i1,g1],[i1,h1]*> ^ t1)) by FINSEQ_1:32
.= (s2 ^ s) ^ (<*[i1,g1],[i1,h1]*> ^ t1) by FINSEQ_1:32
.= ((s2 ^ s) ^ <*[i1,g1],[i1,h1]*>) ^ t1 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A21, A27; :: thesis: verum

end;

suppose A28: len s1 < len s2 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

(len s1) + 1 <> len s2

proof

assume (len s1) + 1 = len s2 ; :: thesis: contradiction
then A29: len (s1 ^ <*[i1,g1]*>) = len s2 by FINSEQ_2:16;
A30: p = (s1 ^ (<*[i1,g1]*> ^ <*[i1,h1]*>)) ^ t1 by A21, FINSEQ_1:def 9
.= ((s1 ^ <*[i1,g1]*>) ^ <*[i1,h1]*>) ^ t1 by FINSEQ_1:32 ;
len <*[i2,(1_ (G . i2))]*> = 1 by FINSEQ_1:39
.= len <*[i1,h1]*> by FINSEQ_1:39 ;
then A31: ( s2 = s1 ^ <*[i1,g1]*> & <*[i2,(1_ (G . i2))]*> = <*[i1,h1]*> & t2 = t1 ) by A22, A29, A30, Lm2;
then [i2,(1_ (G . i2))] = [i1,h1] by FINSEQ_1:76;
then ( i2 = i1 & 1_ (G . i2) = h1 ) by XTUPLE_0:1;
hence contradiction by A1, A21, A22, A31, GROUP_1:def 4; :: thesis: verum

end;

then ( (len s1) + 1 < len s2 or (len s1) + 1 > len s2 ) by XXREAL_0:1;
then ((len s1) + 1) + 1 < (len s2) + 1 by A28, NAT_1:13, XREAL_1:8;
then (len s1) + 2 <= len s2 by NAT_1:13;
then (len s1) + (len <*[i1,g1],[i1,h1]*>) <= len s2 by FINSEQ_1:44;
then A32: len (s1 ^ <*[i1,g1],[i1,h1]*>) <= len s2 by FINSEQ_1:22;
p = s2 ^ (<*[i2,(1_ (G . i2))]*> ^ t2) by A22, FINSEQ_1:32;
then consider s being FinSequence such that
A33: (s1 ^ <*[i1,g1],[i1,h1]*>) ^ s = s2 by A21, A32, FINSEQ_1:47;
set r = s1;
set t = t2;
reconsider s = s as FinSequence of FreeAtoms G by A33, FINSEQ_1:36;
p = (((s1 ^ <*[i1,g1],[i1,h1]*>) ^ s) ^ <*[i2,(1_ (G . i2))]*>) ^ t2 by A22, A33;
then p = ((s1 ^ <*[i1,g1],[i1,h1]*>) ^ s) ^ (<*[i2,(1_ (G . i2))]*> ^ t2) by FINSEQ_1:32
.= (s1 ^ <*[i1,g1],[i1,h1]*>) ^ (s ^ (<*[i2,(1_ (G . i2))]*> ^ t2)) by FINSEQ_1:32
.= (s1 ^ <*[i1,g1],[i1,h1]*>) ^ ((s ^ <*[i2,(1_ (G . i2))]*>) ^ t2) by FINSEQ_1:32 ;
then q1 = (s1 ^ <*[i1,(g1 * h1)]*>) ^ ((s ^ <*[i2,(1_ (G . i2))]*>) ^ t2) by A21, FINSEQ_1:33
.= (s1 ^ <*[i1,(g1 * h1)]*>) ^ (s ^ (<*[i2,(1_ (G . i2))]*> ^ t2)) by FINSEQ_1:32
.= ((s1 ^ <*[i1,(g1 * h1)]*>) ^ s) ^ (<*[i2,(1_ (G . i2))]*> ^ t2) by FINSEQ_1:32
.= (((s1 ^ <*[i1,(g1 * h1)]*>) ^ s) ^ <*[i2,(1_ (G . i2))]*>) ^ t2 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A22, A33; :: thesis: verum

end;

end;

end;

suppose ex s2, t2 being FinSequence of FreeAtoms G ex i2 being Element of I ex g2, h2 being Element of (G . i2) st
( p = (s2 ^ <*[i2,g2],[i2,h2]*>) ^ t2 & q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ t2 ) ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then consider s2, t2 being FinSequence of FreeAtoms G, i2 being Element of I, g2, h2 being Element of (G . i2) such that
A34: ( p = (s2 ^ <*[i2,g2],[i2,h2]*>) ^ t2 & q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ t2 ) ;
len s1 <> len s2

proof

assume A35: len s1 = len s2 ; :: thesis: contradiction
len <*[i1,g1],[i1,h1]*> = 2 by FINSEQ_1:44
.= len <*[i2,g2],[i2,h2]*> by FINSEQ_1:44 ;
then A36: ( s1 = s2 & <*[i1,g1],[i1,h1]*> = <*[i2,g2],[i2,h2]*> & t1 = t2 ) by A21, A34, A35, Lm2;
then ( [i1,g1] = [i2,g2] & [i1,h1] = [i2,h2] ) by FINSEQ_1:77;
then ( i1 = i2 & g1 = g2 & h1 = h2 ) by XTUPLE_0:1;
hence contradiction by A1, A21, A36, A34; :: thesis: verum

end;

per cases then ( len s1 < len s2 or len s2 < len s1 ) by XXREAL_0:1;

suppose len s1 < len s2 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then (len s1) + 1 <= len s2 by NAT_1:13;

per cases then ( (len s1) + 1 < len s2 or (len s1) + 1 = len s2 ) by XXREAL_0:1;

suppose (len s1) + 1 < len s2 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then ((len s1) + 1) + 1 < (len s2) + 1 by XREAL_1:8;
then (len s1) + 2 <= len s2 by NAT_1:13;
then (len s1) + (len <*[i1,g1],[i1,h1]*>) <= len s2 by FINSEQ_1:44;
then A37: len (s1 ^ <*[i1,g1],[i1,h1]*>) <= len s2 by FINSEQ_1:22;
p = s2 ^ (<*[i2,g2],[i2,h2]*> ^ t2) by A34, FINSEQ_1:32;
then consider s being FinSequence such that
A38: (s1 ^ <*[i1,g1],[i1,h1]*>) ^ s = s2 by A21, A37, FINSEQ_1:47;
set r = s1;
set t = t2;
reconsider s = s as FinSequence of FreeAtoms G by A38, FINSEQ_1:36;
p = (((s1 ^ <*[i1,g1],[i1,h1]*>) ^ s) ^ <*[i2,g2],[i2,h2]*>) ^ t2 by A34, A38;
then p = ((s1 ^ <*[i1,g1],[i1,h1]*>) ^ s) ^ (<*[i2,g2],[i2,h2]*> ^ t2) by FINSEQ_1:32
.= (s1 ^ <*[i1,g1],[i1,h1]*>) ^ (s ^ (<*[i2,g2],[i2,h2]*> ^ t2)) by FINSEQ_1:32
.= (s1 ^ <*[i1,g1],[i1,h1]*>) ^ ((s ^ <*[i2,g2],[i2,h2]*>) ^ t2) by FINSEQ_1:32 ;
then q1 = (s1 ^ <*[i1,(g1 * h1)]*>) ^ ((s ^ <*[i2,g2],[i2,h2]*>) ^ t2) by A21, FINSEQ_1:33
.= (s1 ^ <*[i1,(g1 * h1)]*>) ^ (s ^ (<*[i2,g2],[i2,h2]*> ^ t2)) by FINSEQ_1:32
.= ((s1 ^ <*[i1,(g1 * h1)]*>) ^ s) ^ (<*[i2,g2],[i2,h2]*> ^ t2) by FINSEQ_1:32
.= (((s1 ^ <*[i1,(g1 * h1)]*>) ^ s) ^ <*[i2,g2],[i2,h2]*>) ^ t2 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A34, A38; :: thesis: verum

end;

suppose (len s1) + 1 = len s2 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then A39: len (s1 ^ <*[i1,g1]*>) = len s2 by FINSEQ_2:16;
A40: p = (s1 ^ (<*[i1,g1]*> ^ <*[i1,h1]*>)) ^ t1 by A21, FINSEQ_1:def 9
.= ((s1 ^ <*[i1,g1]*>) ^ <*[i1,h1]*>) ^ t1 by FINSEQ_1:32 ;
A41: p = (s2 ^ (<*[i2,g2]*> ^ <*[i2,h2]*>)) ^ t2 by A34, FINSEQ_1:def 9
.= s2 ^ ((<*[i2,g2]*> ^ <*[i2,h2]*>) ^ t2) by FINSEQ_1:32
.= s2 ^ (<*[i2,g2]*> ^ (<*[i2,h2]*> ^ t2)) by FINSEQ_1:32
.= (s2 ^ <*[i2,g2]*>) ^ (<*[i2,h2]*> ^ t2) by FINSEQ_1:32 ;
len <*[i1,h1]*> = 1 by FINSEQ_1:39
.= len <*[i2,g2]*> by FINSEQ_1:39 ;
then A42: ( s1 ^ <*[i1,g1]*> = s2 & <*[i1,h1]*> = <*[i2,g2]*> & t1 = <*[i2,h2]*> ^ t2 ) by A40, A41, A39, Lm2;
then [i1,h1] = [i2,g2] by FINSEQ_1:76;
then A43: ( i1 = i2 & h1 = g2 ) by XTUPLE_0:1;
then reconsider h = h2 as Element of (G . i1) ;
set f = g1;
set g = h1;
set s = s1;
set t = t2;
A44: p = ((s1 ^ <*[i1,g1],[i1,h1]*>) ^ <*[i2,h2]*>) ^ t2 by A21, A42, FINSEQ_1:32
.= (s1 ^ (<*[i1,g1],[i1,h1]*> ^ <*[i2,h2]*>)) ^ t2 by FINSEQ_1:32
.= (s1 ^ <*[i1,g1],[i1,h1],[i1,h]*>) ^ t2 by A43, FINSEQ_1:43 ;
A45: q1 = ((s1 ^ <*[i1,(g1 * h1)]*>) ^ <*[i1,h]*>) ^ t2 by A43, A21, A42, FINSEQ_1:32
.= (s1 ^ (<*[i1,(g1 * h1)]*> ^ <*[i1,h]*>)) ^ t2 by FINSEQ_1:32
.= (s1 ^ <*[i1,(g1 * h1)],[i1,h]*>) ^ t2 by FINSEQ_1:def 9 ;
q2 = (s1 ^ (<*[i1,g1]*> ^ <*[i1,(h1 * h)]*>)) ^ t2 by A34, A42, A43, FINSEQ_1:32
.= (s1 ^ <*[i1,g1],[i1,(h1 * h)]*>) ^ t2 by FINSEQ_1:def 9 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A44, A45; :: thesis: verum

end;

end;

end;

suppose len s2 < len s1 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then (len s2) + 1 <= len s1 by NAT_1:13;

per cases then ( (len s2) + 1 < len s1 or (len s2) + 1 = len s1 ) by XXREAL_0:1;

suppose (len s2) + 1 < len s1 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then ((len s2) + 1) + 1 < (len s1) + 1 by XREAL_1:8;
then (len s2) + 2 <= len s1 by NAT_1:13;
then (len s2) + (len <*[i2,g2],[i2,h2]*>) <= len s1 by FINSEQ_1:44;
then A46: len (s2 ^ <*[i2,g2],[i2,h2]*>) <= len s1 by FINSEQ_1:22;
p = s1 ^ (<*[i1,g1],[i1,h1]*> ^ t1) by A21, FINSEQ_1:32;
then consider s being FinSequence such that
A47: (s2 ^ <*[i2,g2],[i2,h2]*>) ^ s = s1 by A34, A46, FINSEQ_1:47;
set r = s2;
set t = t1;
reconsider s = s as FinSequence of FreeAtoms G by A47, FINSEQ_1:36;
p = (((s2 ^ <*[i2,g2],[i2,h2]*>) ^ s) ^ <*[i1,g1],[i1,h1]*>) ^ t1 by A21, A47;
then p = ((s2 ^ <*[i2,g2],[i2,h2]*>) ^ s) ^ (<*[i1,g1],[i1,h1]*> ^ t1) by FINSEQ_1:32
.= (s2 ^ <*[i2,g2],[i2,h2]*>) ^ (s ^ (<*[i1,g1],[i1,h1]*> ^ t1)) by FINSEQ_1:32
.= (s2 ^ <*[i2,g2],[i2,h2]*>) ^ ((s ^ <*[i1,g1],[i1,h1]*>) ^ t1) by FINSEQ_1:32 ;
then q2 = (s2 ^ <*[i2,(g2 * h2)]*>) ^ ((s ^ <*[i1,g1],[i1,h1]*>) ^ t1) by A34, FINSEQ_1:33
.= (s2 ^ <*[i2,(g2 * h2)]*>) ^ (s ^ (<*[i1,g1],[i1,h1]*> ^ t1)) by FINSEQ_1:32
.= ((s2 ^ <*[i2,(g2 * h2)]*>) ^ s) ^ (<*[i1,g1],[i1,h1]*> ^ t1) by FINSEQ_1:32
.= (((s2 ^ <*[i2,(g2 * h2)]*>) ^ s) ^ <*[i1,g1],[i1,h1]*>) ^ t1 by FINSEQ_1:32 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A21, A47; :: thesis: verum

end;

suppose (len s2) + 1 = len s1 ; :: thesis: ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) )

then A48: len (s2 ^ <*[i2,g2]*>) = len s1 by FINSEQ_2:16;
A49: p = (s2 ^ (<*[i2,g2]*> ^ <*[i2,h2]*>)) ^ t2 by A34, FINSEQ_1:def 9
.= ((s2 ^ <*[i2,g2]*>) ^ <*[i2,h2]*>) ^ t2 by FINSEQ_1:32 ;
A50: p = (s1 ^ (<*[i1,g1]*> ^ <*[i1,h1]*>)) ^ t1 by A21, FINSEQ_1:def 9
.= s1 ^ ((<*[i1,g1]*> ^ <*[i1,h1]*>) ^ t1) by FINSEQ_1:32
.= s1 ^ (<*[i1,g1]*> ^ (<*[i1,h1]*> ^ t1)) by FINSEQ_1:32
.= (s1 ^ <*[i1,g1]*>) ^ (<*[i1,h1]*> ^ t1) by FINSEQ_1:32 ;
len <*[i2,h2]*> = 1 by FINSEQ_1:39
.= len <*[i1,g1]*> by FINSEQ_1:39 ;
then A51: ( s2 ^ <*[i2,g2]*> = s1 & <*[i2,h2]*> = <*[i1,g1]*> & t2 = <*[i1,h1]*> ^ t1 ) by A49, A50, A48, Lm2;
then [i2,h2] = [i1,g1] by FINSEQ_1:76;
then A52: ( i2 = i1 & h2 = g1 ) by XTUPLE_0:1;
then reconsider h = h1 as Element of (G . i2) ;
set f = g2;
set g = h2;
set s = s2;
set t = t1;
A53: p = ((s2 ^ <*[i2,g2],[i2,h2]*>) ^ <*[i1,h1]*>) ^ t1 by A34, A51, FINSEQ_1:32
.= (s2 ^ (<*[i2,g2],[i2,h2]*> ^ <*[i1,h1]*>)) ^ t1 by FINSEQ_1:32
.= (s2 ^ <*[i2,g2],[i2,h2],[i2,h]*>) ^ t1 by A52, FINSEQ_1:43 ;
A54: q2 = ((s2 ^ <*[i2,(g2 * h2)]*>) ^ <*[i2,h]*>) ^ t1 by A52, A34, A51, FINSEQ_1:32
.= (s2 ^ (<*[i2,(g2 * h2)]*> ^ <*[i2,h]*>)) ^ t1 by FINSEQ_1:32
.= (s2 ^ <*[i2,(g2 * h2)],[i2,h]*>) ^ t1 by FINSEQ_1:def 9 ;
q1 = (s2 ^ (<*[i2,g2]*> ^ <*[i2,(h2 * h)]*>)) ^ t1 by A21, A51, A52, FINSEQ_1:32
.= (s2 ^ <*[i2,g2],[i2,(h2 * h)]*>) ^ t1 by FINSEQ_1:def 9 ;
hence ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex f, g, h being Element of (G . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or 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 ) ) ) ) ) ) by A53, A54; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;