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 } ;

now

assume A1: 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
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;
k2 in NAT by ORDINAL1:def 13;
hence x in Z1 by A1, A4; :: 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;

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 Th1; :: thesis: verum