let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H st p ^ q is_a_normal_form_wrt ReductionRel H & len p <> 0 & len q <> 0 holds
(p . (len p)) `1 <> (q . 1) `1
let H be Group-like associative multMagma-Family of I; :: thesis: for p, q being FinSequence of FreeAtoms H st p ^ q is_a_normal_form_wrt ReductionRel H & len p <> 0 & len q <> 0 holds
(p . (len p)) `1 <> (q . 1) `1
let p, q be FinSequence of FreeAtoms H; :: thesis: ( p ^ q is_a_normal_form_wrt ReductionRel H & len p <> 0 & len q <> 0 implies (p . (len p)) `1 <> (q . 1) `1 )
assume A1: ( p ^ q is_a_normal_form_wrt ReductionRel H & len p <> 0 & len q <> 0 ) ; :: thesis: (p . (len p)) `1 <> (q . 1) `1
then ( 1 <= len p & 1 <= len q ) by NAT_1:14;
then ( len p in dom p & 1 in dom q ) by FINSEQ_3:25;
then ( p . (len p) in rng p & q . 1 in rng q ) by FUNCT_1:3;
then A2: ( p . (len p) in FreeAtoms H & q . 1 in FreeAtoms H ) ;
then consider x1, y1 being object such that
A3: p . (len p) = [x1,y1] by RELAT_1:def 1;
consider x2, y2 being object such that
A4: q . 1 = [x2,y2] by A2, RELAT_1:def 1;
x1 in dom H by A2, A3, Th7;
then reconsider i = x1 as Element of I ;
assume (p . (len p)) `1 = (q . 1) `1 ; :: thesis: contradiction
then x1 = (q . 1) `1 by A3;
then A5: x2 = i by A4;
reconsider g = y1 as Element of (H . i) by A2, A3, Th9;
reconsider h = y2 as Element of (H . i) by A2, A4, A5, Th9;
set l = (len p) -' 1;
A6: p ^ q = ((p | ((len p) -' 1)) ^ (p /^ ((len p) -' 1))) ^ q by RFINSEQ:8
.= ((p | ((len p) -' 1)) ^ (p /^ ((len p) -' 1))) ^ ((q | 1) ^ (q /^ 1)) by RFINSEQ:8
.= (((p | ((len p) -' 1)) ^ (p /^ ((len p) -' 1))) ^ (q | 1)) ^ (q /^ 1) by FINSEQ_1:32
.= ((p | ((len p) -' 1)) ^ ((p /^ ((len p) -' 1)) ^ (q | 1))) ^ (q /^ 1) by FINSEQ_1:32
.= ((p | ((len p) -' 1)) ^ (<*(p . (len p))*> ^ (q | 1))) ^ (q /^ 1) by A1, Th2
.= ((p | ((len p) -' 1)) ^ (<*(p . (len p))*> ^ <*(q . 1)*>)) ^ (q /^ 1) by A1, Th1
.= ((p | ((len p) -' 1)) ^ <*[i,g],[i,h]*>) ^ (q /^ 1) by A3, A4, A5, FINSEQ_1:def 9 ;
set b = ((p | ((len p) -' 1)) ^ <*[i,(g * h)]*>) ^ (q /^ 1);
[i,(g * h)] in FreeAtoms H by Th9;
then <*[i,(g * h)]*> is FinSequence of FreeAtoms H by FINSEQ_1:74;
then ((p | ((len p) -' 1)) ^ <*[i,(g * h)]*>) ^ (q /^ 1) is FinSequence of FreeAtoms H by FINSEQ_1:75;
then [(p ^ q),(((p | ((len p) -' 1)) ^ <*[i,(g * h)]*>) ^ (q /^ 1))] in ReductionRel H by A6, Def3;
hence contradiction by A1, REWRITE1:def 5; :: thesis: verum