let n be Nat; :: thesis:
let x be object ; :: thesis:
let Y be set ; :: thesis:
let f be sequence of Y; :: thesis:
set Z = { (f . k2) where k2 is Nat : n <= k2 } ;

now :: thesis:

assume A1: for k1 being Nat holds x in f . (n + k1) ; :: thesis:

now :: thesis:

let Z1 be set ; :: thesis:
assume Z1 in { (f . k2) where k2 is Nat : n <= k2 } ; :: thesis:
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:

end;

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

end;

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 Z ) by Th1; :: thesis: