let I be non empty set ; :: thesis: for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G holds
( not ReductionRel G reduces p,q or p = q or len q < len p )
let G be Group-like multMagma-Family of I; :: thesis: for p, q being FinSequence of FreeAtoms G holds
( not ReductionRel G reduces p,q or p = q or len q < len p )
let p, q be FinSequence of FreeAtoms G; :: thesis: ( not ReductionRel G reduces p,q or p = q or len q < len p )
assume A1: ( ReductionRel G reduces p,q & p <> q ) ; :: thesis: len q < len p
then consider r being RedSequence of ReductionRel G such that
A2: ( r . 1 = p & r . (len r) = q ) by REWRITE1:def 3;
A3: len r <> 1 by A1, A2;

now :: thesis: for x being object st x in dom r holds
r . x is FinSequence

let x be object ; :: thesis: ( x in dom r implies r . b₁ is FinSequence )
assume A4: x in dom r ; :: thesis: r . b₁ is FinSequence
then reconsider k = x as Nat ;
( 1 <= k & k <= len r ) by A4, FINSEQ_3:25;

per cases then ( k < len r or k = len r ) by XXREAL_0:1;

suppose k < len r ; :: thesis: r . b₁ is FinSequence

then A5: k + 1 <= len r by NAT_1:13;
1 + 0 <= k + 1 by XREAL_1:7;
then k + 1 in dom r by A5, FINSEQ_3:25;
then [(r . k),(r . (k + 1))] in ReductionRel G by A4, REWRITE1:def 2;
hence r . x is FinSequence by Th31; :: thesis: verum

end;

suppose A6: k = len r ; :: thesis: r . b₁ is FinSequence

then reconsider k9 = k - 1 as Nat by INT_1:74;
A7: 2 - 1 <= k9 by A3, A6, NAT_1:23, XREAL_1:9;
k9 <= (len r) - 0 by A6, XREAL_1:10;
then k9 in dom r by A7, FINSEQ_3:25;
then [(r . k9),(r . (k9 + 1))] in ReductionRel G by A4, REWRITE1:def 2;
hence r . x is FinSequence by Th31; :: thesis: verum

end;

end;

end;

then reconsider r = r as FinSequence-yielding FinSequence by PRE_POLY:def 3;
defpred S₁[ Nat] means ( $1 < len r implies (len (r . ($1 + 1))) + $1 = len p );
A8: S₁[ 0 ] by A2;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: ( S₁[k] & k + 1 < len r ) ; :: thesis: (len (r . ((k + 1) + 1))) + (k + 1) = len p
then (k + 1) - 1 < (len r) - 0 by XREAL_1:14;
then A11: len p = (len (r . (k + 1))) + k by A10;
A12: (k + 1) + 1 <= len r by A10, NAT_1:13;
A13: (k + 1) + 0 <= (k + 1) + 1 by XREAL_1:6;
A14: 0 + 1 <= k + 1 by XREAL_1:6;
then ( 1 <= (k + 1) + 1 & k + 1 <= len r ) by A12, A13, XXREAL_0:2;
then ( k + 1 in dom r & (k + 1) + 1 in dom r ) by A12, A14, FINSEQ_3:25;
then [(r . (k + 1)),(r . ((k + 1) + 1))] in ReductionRel G by REWRITE1:def 2;
then len (r . (k + 1)) = (len (r . ((k + 1) + 1))) + 1 by Th35;
hence (len (r . ((k + 1) + 1))) + (k + 1) = len p by A11; :: thesis: verum

end;

A15: for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A9);
reconsider k = (len r) - 1 as Nat by INT_1:74;
k < (len r) - 0 by XREAL_1:15;
then A16: len p = (len (r . (k + 1))) + k by A15
.= (len q) + k by A2 ;
assume len q >= len p ; :: thesis: contradiction
then (len q) + 0 >= (len q) + k by A16;
then k = 0 by XREAL_1:6;
hence contradiction by A3; :: thesis: verum