let n, m be Element of NAT ; :: thesis: for Y being set
for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k }
let Y be set ; :: thesis: for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k }
n <= n + m by NAT_1:11;
hence for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k } ; :: thesis: verum