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_{1} being set holds [(f . b_{1}),(f . (b_{1} + 1))] in the reduction of X

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

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

end;

suppose
f is the carrier of X -valued
; :: thesis: not for b_{1} being set holds [(f . b_{1}),(f . (b_{1} + 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;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

suppose
not f is the carrier of X -valued
; :: thesis: not for b_{1} being set holds [(f . b_{1}),(f . (b_{1} + 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;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