now :: thesis: for f being ManySortedSet of NAT holds
not for i being Nat holds [(f . i),(f . (i + 1))] in ReductionRel G

set R = ReductionRel G;
A1: field (ReductionRel G) c= the carrier of ((FreeAtoms G) *+^+<0>) \/ the carrier of ((FreeAtoms G) *+^+<0>) by RELSET_1:8;
given f being ManySortedSet of NAT such that A2: for i being Nat holds [(f . i),(f . (i + 1))] in ReductionRel G ; :: thesis: contradiction
[(f . 0),(f . (0 + 1))] in ReductionRel G by A2;
then f . 0 in field (ReductionRel G) by RELAT_1:15;
then f . 0 in the carrier of ((FreeAtoms G) *+^+<0>) by A1;
then f . 0 in (FreeAtoms G) * by MONOID_0:61;
then reconsider p = f . 0 as FinSequence of FreeAtoms G by FINSEQ_1:def 11;
defpred S₁[ Nat] means ex q being FinSequence of FreeAtoms G st
( q = f . I & (len q) + I = len p );
A3: S₁[ 0 ]

proof

take p ; :: thesis: ( p = f . 0 & (len p) + 0 = len p )
thus ( p = f . 0 & (len p) + 0 = len p ) ; :: thesis: verum

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: [(f . n),(f . (n + 1))] in ReductionRel G by A2;
then f . (n + 1) in field (ReductionRel G) by RELAT_1:15;
then f . (n + 1) in the carrier of ((FreeAtoms G) *+^+<0>) by A1;
then f . (n + 1) in (FreeAtoms G) * by MONOID_0:61;
then reconsider q = f . (n + 1) as FinSequence of FreeAtoms G by FINSEQ_1:def 11;
take q ; :: thesis: ( q = f . (n + 1) & (len q) + (n + 1) = len p )
consider q9 being FinSequence of FreeAtoms G such that
A7: ( q9 = f . n & (len q9) + n = len p ) by A5;
len q9 = (len q) + 1 by A6, A7, Th35;
hence ( q = f . (n + 1) & (len q) + (n + 1) = len p ) by A7; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
then consider q being FinSequence of FreeAtoms G such that
A8: ( q = f . ((len p) + 1) & (len q) + ((len p) + 1) = len p ) ;
(len q) + 1 = 0 by A8;
hence contradiction ; :: thesis: verum

end;

hence ReductionRel G is strongly-normalizing by REWRITE1:def 15; :: thesis: verum