let n be Nat; :: thesis: for x being object

for Y being set

for f being sequence of Y holds

( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

let x be object ; :: thesis: for Y being set

for f being sequence of Y holds

( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

let Y be set ; :: thesis: for f being sequence of Y holds

( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

let f be sequence of Y; :: thesis: ( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

set Z = { (f . k2) where k2 is Nat : n <= k2 } ;

x in Z ) by Th1; :: thesis: verum

for Y being set

for f being sequence of Y holds

( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

let x be object ; :: thesis: for Y being set

for f being sequence of Y holds

( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

let Y be set ; :: thesis: for f being sequence of Y holds

( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

let f be sequence of Y; :: thesis: ( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z )

set Z = { (f . k2) where k2 is Nat : n <= k2 } ;

now :: thesis: ( ( for k1 being Nat holds x in f . (n + k1) ) implies for Z1 being set st Z1 in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z1 )

hence
( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds x in Z1 )

assume A1:
for k1 being Nat holds x in f . (n + k1)
; :: thesis: for Z1 being set st Z1 in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z1

x in Z1 ; :: thesis: verum

end;x in Z1

now :: thesis: for Z1 being set st Z1 in { (f . k2) where k2 is Nat : n <= k2 } holds

x in Z1

hence
for Z1 being set st Z1 in { (f . k2) where k2 is Nat : n <= k2 } holds x in Z1

let Z1 be set ; :: thesis: ( Z1 in { (f . k2) where k2 is Nat : n <= k2 } implies x in Z1 )

assume Z1 in { (f . k2) where k2 is Nat : n <= k2 } ; :: thesis: x in Z1

then consider k1 being Nat such that

A2: Z1 = f . k1 and

A3: n <= k1 ;

ex m being Nat st k1 = n + m by A3, NAT_1:10;

then consider k2 being Nat such that

A4: Z1 = f . (n + k2) by A2;

thus x in Z1 by A1, A4; :: thesis: verum

end;assume Z1 in { (f . k2) where k2 is Nat : n <= k2 } ; :: thesis: x in Z1

then consider k1 being Nat such that

A2: Z1 = f . k1 and

A3: n <= k1 ;

ex m being Nat st k1 = n + m by A3, NAT_1:10;

then consider k2 being Nat such that

A4: Z1 = f . (n + k2) by A2;

thus x in Z1 by A1, A4; :: thesis: verum

x in Z1 ; :: thesis: verum

x in Z ) by Th1; :: thesis: verum