let X be ARS ; :: thesis: ( X is SN implies the reduction of X is strongly-normalizing )
set R = the reduction of X;
set A = the carrier of X;
A0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
assume A1: for f being Function of NAT, the carrier of X holds
not for i being Nat holds f . i ==> f . (i + 1) ; :: according to ABSRED_0:def 15 :: thesis: the reduction of X is strongly-normalizing
let f be ManySortedSet of NAT ; :: according to REWRITE1:def 15 :: thesis: not for b₁ being set holds [(f . b₁),(f . (b₁ + 1))] in the reduction of X

per cases ( f is the carrier of X -valued or not f is the carrier of X -valued ) ;

suppose f is the carrier of X -valued ; :: thesis: not for b₁ being set holds [(f . b₁),(f . (b₁ + 1))] in the reduction of X

then ( rng f c= the carrier of X & dom f = NAT ) by RELAT_1:def 19, PARTFUN1:def 2;
then reconsider g = f as Function of NAT, the carrier of X by FUNCT_2:2;
consider i being Nat such that
A2: not g . i ==> g . (i + 1) by A1;
take i ; :: thesis: not [(f . i),(f . (i + 1))] in the reduction of X
thus not [(f . i),(f . (i + 1))] in the reduction of X by A2; :: thesis: verum

end;

suppose not f is the carrier of X -valued ; :: thesis: not for b₁ being set holds [(f . b₁),(f . (b₁ + 1))] in the reduction of X

then consider a being object such that
A3: ( a in rng f & not a in the carrier of X ) by TARSKI:def 3, RELAT_1:def 19;
consider i being object such that
A4: ( i in dom f & a = f . i ) by A3, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A4;
take i ; :: thesis: not [(f . i),(f . (i + 1))] in the reduction of X
assume [(f . i),(f . (i + 1))] in the reduction of X ; :: thesis: contradiction
then a in field the reduction of X by A4, RELAT_1:15;
hence contradiction by A0, A3; :: thesis: verum

end;

end;