let X be non empty set ; :: thesis: for s being sequence of X
for n being Nat holds s . n in rng s
let s be sequence of X; :: thesis: for n being Nat holds s . n in rng s
let n be Nat; :: thesis: s . n in rng s
n in NAT by ORDINAL1:def 12;
hence s . n in rng s by FUNCT_2:112; :: thesis: verum