let n, m be Nat; :: thesis: for Y being set

for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k }

let Y be set ; :: thesis: for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k }

n <= n + m by NAT_1:11;

hence for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k } ; :: thesis: verum

for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k }

let Y be set ; :: thesis: for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k }

n <= n + m by NAT_1:11;

hence for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k } ; :: thesis: verum