let R be non empty RelStr ; :: thesis: for s being sequence of R

for j being Nat st s is descending holds

s ^\ j is descending

let s1 be sequence of R; :: thesis: for j being Nat st s1 is descending holds

s1 ^\ j is descending

let j be Nat; :: thesis: ( s1 is descending implies s1 ^\ j is descending )

assume A1: s1 is descending ; :: thesis: s1 ^\ j is descending

set s2 = s1 ^\ j;

set IR = the InternalRel of R;

for j being Nat st s is descending holds

s ^\ j is descending

let s1 be sequence of R; :: thesis: for j being Nat st s1 is descending holds

s1 ^\ j is descending

let j be Nat; :: thesis: ( s1 is descending implies s1 ^\ j is descending )

assume A1: s1 is descending ; :: thesis: s1 ^\ j is descending

set s2 = s1 ^\ j;

set IR = the InternalRel of R;

now :: thesis: for n being Nat holds

( (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n & [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R )

hence
s1 ^\ j is descending
; :: thesis: verum( (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n & [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R )

let n be Nat; :: thesis: ( (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n & [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R )

set nj = n + j;

A2: (s1 ^\ j) . n = s1 . (n + j) by NAT_1:def 3;

A3: (s1 ^\ j) . (n + 1) = s1 . ((n + 1) + j) by NAT_1:def 3

.= s1 . ((n + j) + 1) ;

hence (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n by A1, A2; :: thesis: [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R

thus [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R by A1, A2, A3; :: thesis: verum

end;set nj = n + j;

A2: (s1 ^\ j) . n = s1 . (n + j) by NAT_1:def 3;

A3: (s1 ^\ j) . (n + 1) = s1 . ((n + 1) + j) by NAT_1:def 3

.= s1 . ((n + j) + 1) ;

hence (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n by A1, A2; :: thesis: [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R

thus [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R by A1, A2, A3; :: thesis: verum