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

A00: now

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

now

let Z1 be set ; :: thesis: ( Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } implies x in Z1 )
assume Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } ; :: thesis: x in Z1
then consider k1 being Element of NAT such that
B1: ( Z1 = f . k1 & n <= k1 ) ;
ex m being Nat st k1 = n + m by B1, NAT_1:10;
then consider k2 being Nat such that
B2: Z1 = f . (n + k2) by B1;
k2 in NAT by ORDINAL1:def 13;
hence x in Z1 by B0, B2; :: thesis: verum

end;

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

end;

( ( for Z1 being set st Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } holds
x in Z1 ) implies for k1 being Element of NAT holds x in f . (n + k1) ) by Th5;
hence ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Element of NAT : n <= k2 } holds
x in Z ) by A00; :: thesis: verum