let x be object ; :: thesis: ( x in { (seq .(j + k)) where k is Nat : n <= k } implies x in { (seq . k1) where k1 is Nat : j + n <= k1 } ) assume
x in { (seq .(j + k)) where k is Nat : n <= k }
; :: thesis: x in { (seq . k1) where k1 is Nat : j + n <= k1 } then consider k being Nat such that A7:
x = seq .(j + k)and A8:
n <= k
;
j + n <= j + k
byA8, XREAL_1:6; hence
x in { (seq . k1) where k1 is Nat : j + n <= k1 } byA7; :: thesis: verum
end;
then { (seq .(j + k)) where k is Nat : n <= k } c= { (seq . k) where k is Nat : j + n <= k }
; then A9:
{ (seq .(j + k)) where k is Nat : n <= k } = { (seq . k) where k is Nat : j + n <= k } byA6, XBOOLE_0:def 10;